Termination proof of /tmp/tmpafmwJo/LengthOfFiniteLists

Termination of the following Term Rewriting System could be proven:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, V1) → U12(isNatList(V1))
U12(tt) → tt
U21(tt, V1) → U22(isNat(V1))
U22(tt) → tt
U31(tt, V) → U32(isNatList(V))
U32(tt) → tt
U41(tt, V1, V2) → U42(isNat(V1), V2)
U42(tt, V2) → U43(isNatIList(V2))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNat(V1), V2)
U52(tt, V2) → U53(isNatList(V2))
U53(tt) → tt
U61(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
isNatIList(V) → U31(isNatIListKind(V), V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → and(isNatKind(V1), isNatIListKind(V2))
isNatKind(0) → tt
isNatKind(length(V1)) → isNatIListKind(V1)
isNatKind(s(V1)) → isNatKind(V1)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
length(nil) → 0
length(cons(N, L)) → U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

The replacement map contains the following entries:

zeros: empty set
cons: {1}
0: empty set
U11: {1}
tt: empty set
U12: {1}
isNatList: empty set
U21: {1}
U22: {1}
isNat: empty set
U31: {1}
U32: {1}
U41: {1}
U42: {1}
U43: {1}
isNatIList: empty set
U51: {1}
U52: {1}
U53: {1}
U61: {1}
s: {1}
length: {1}
and: {1}
isNatIListKind: empty set
isNatKind: empty set
nil: empty set

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

Context-sensitive rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, V1) → U12(isNatList(V1))
U12(tt) → tt
U21(tt, V1) → U22(isNat(V1))
U22(tt) → tt
U31(tt, V) → U32(isNatList(V))
U32(tt) → tt
U41(tt, V1, V2) → U42(isNat(V1), V2)
U42(tt, V2) → U43(isNatIList(V2))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNat(V1), V2)
U52(tt, V2) → U53(isNatList(V2))
U53(tt) → tt
U61(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
isNatIList(V) → U31(isNatIListKind(V), V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → and(isNatKind(V1), isNatIListKind(V2))
isNatKind(0) → tt
isNatKind(length(V1)) → isNatIListKind(V1)
isNatKind(s(V1)) → isNatKind(V1)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
length(nil) → 0
length(cons(N, L)) → U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

The replacement map contains the following entries:

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

  ↳ Incomplete Giesl Middeldorp-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {U12, U22, U32, U43, U53, s, length, U12¹, U22¹, U32¹, U43¹, U53¹, LENGTH} are replacing on all positions.
For all symbols f in {cons, U11, U21, U31, U41, U42, U51, U52, U61, and, U11¹, U21¹, U31¹, U42¹, U41¹, U52¹, U51¹, U61¹, AND} we have µ(f) = {1}.
The symbols in {isNatList, isNat, isNatIList, isNatIListKind, isNatKind, ISNATLIST, ISNAT, ISNATILIST, ISNATILISTKIND, ISNATKIND, U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DP_o are:

U11¹(tt, V1) → U12¹(isNatList(V1))
U11¹(tt, V1) → ISNATLIST(V1)
U21¹(tt, V1) → U22¹(isNat(V1))
U21¹(tt, V1) → ISNAT(V1)
U31¹(tt, V) → U32¹(isNatList(V))
U31¹(tt, V) → ISNATLIST(V)
U41¹(tt, V1, V2) → U42¹(isNat(V1), V2)
U41¹(tt, V1, V2) → ISNAT(V1)
U42¹(tt, V2) → U43¹(isNatIList(V2))
U42¹(tt, V2) → ISNATILIST(V2)
U51¹(tt, V1, V2) → U52¹(isNat(V1), V2)
U51¹(tt, V1, V2) → ISNAT(V1)
U52¹(tt, V2) → U53¹(isNatList(V2))
U52¹(tt, V2) → ISNATLIST(V2)
U61¹(tt, L) → LENGTH(L)
ISNAT(length(V1)) → U11¹(isNatIListKind(V1), V1)
ISNAT(length(V1)) → ISNATILISTKIND(V1)
ISNAT(s(V1)) → U21¹(isNatKind(V1), V1)
ISNAT(s(V1)) → ISNATKIND(V1)
ISNATILIST(V) → U31¹(isNatIListKind(V), V)
ISNATILIST(V) → ISNATILISTKIND(V)
ISNATILIST(cons(V1, V2)) → U41¹(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
ISNATILIST(cons(V1, V2)) → AND(isNatKind(V1), isNatIListKind(V2))
ISNATILIST(cons(V1, V2)) → ISNATKIND(V1)
ISNATILISTKIND(cons(V1, V2)) → AND(isNatKind(V1), isNatIListKind(V2))
ISNATILISTKIND(cons(V1, V2)) → ISNATKIND(V1)
ISNATKIND(length(V1)) → ISNATILISTKIND(V1)
ISNATKIND(s(V1)) → ISNATKIND(V1)
ISNATLIST(cons(V1, V2)) → U51¹(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
ISNATLIST(cons(V1, V2)) → AND(isNatKind(V1), isNatIListKind(V2))
ISNATLIST(cons(V1, V2)) → ISNATKIND(V1)
LENGTH(cons(N, L)) → U61¹(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)
LENGTH(cons(N, L)) → AND(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N)))
LENGTH(cons(N, L)) → AND(isNatList(L), isNatIListKind(L))
LENGTH(cons(N, L)) → ISNATLIST(L)

The collapsing dependency pairs are DP_c:

U61¹(tt, L) → L
AND(tt, X) → X

The hidden terms of R are:

zeros
isNatIListKind(V2)

Every hiding context is built from:

and on positions {1}

Hence, the new unhiding pairs DP_u are :

U61¹(tt, L) → U(L)
AND(tt, X) → U(X)
U(and(x_0, x_1)) → U(x_0)
U(zeros) → ZEROS
U(isNatIListKind(V2)) → ISNATILISTKIND(V2)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, V1) → U12(isNatList(V1))
U12(tt) → tt
U21(tt, V1) → U22(isNat(V1))
U22(tt) → tt
U31(tt, V) → U32(isNatList(V))
U32(tt) → tt
U41(tt, V1, V2) → U42(isNat(V1), V2)
U42(tt, V2) → U43(isNatIList(V2))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNat(V1), V2)
U52(tt, V2) → U53(isNatList(V2))
U53(tt) → tt
U61(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
isNatIList(V) → U31(isNatIListKind(V), V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → and(isNatKind(V1), isNatIListKind(V2))
isNatKind(0) → tt
isNatKind(length(V1)) → isNatIListKind(V1)
isNatKind(s(V1)) → isNatKind(V1)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
length(nil) → 0
length(cons(N, L)) → U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 4 SCCs with 20 less nodes.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

          ↳ QCSDP

          ↳ QCSDP

          ↳ QCSDP

  ↳ Incomplete Giesl Middeldorp-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {U12, U22, U32, U43, U53, s, length} are replacing on all positions.
For all symbols f in {cons, U11, U21, U31, U41, U42, U51, U52, U61, and, AND} we have µ(f) = {1}.
The symbols in {isNatList, isNat, isNatIList, isNatIListKind, isNatKind, U, ISNATILISTKIND, ISNATKIND} are not replacing on any position.

The TRS P consists of the following rules:

AND(tt, X) → U(X)
U(and(x_0, x_1)) → U(x_0)
U(isNatIListKind(V2)) → ISNATILISTKIND(V2)
ISNATILISTKIND(cons(V1, V2)) → AND(isNatKind(V1), isNatIListKind(V2))
ISNATILISTKIND(cons(V1, V2)) → ISNATKIND(V1)
ISNATKIND(length(V1)) → ISNATILISTKIND(V1)
ISNATKIND(s(V1)) → ISNATKIND(V1)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, V1) → U12(isNatList(V1))
U12(tt) → tt
U21(tt, V1) → U22(isNat(V1))
U22(tt) → tt
U31(tt, V) → U32(isNatList(V))
U32(tt) → tt
U41(tt, V1, V2) → U42(isNat(V1), V2)
U42(tt, V2) → U43(isNatIList(V2))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNat(V1), V2)
U52(tt, V2) → U53(isNatList(V2))
U53(tt) → tt
U61(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
isNatIList(V) → U31(isNatIListKind(V), V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → and(isNatKind(V1), isNatIListKind(V2))
isNatKind(0) → tt
isNatKind(length(V1)) → isNatIListKind(V1)
isNatKind(s(V1)) → isNatKind(V1)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
length(nil) → 0
length(cons(N, L)) → U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

Q is empty.

Using the order
Polynomial interpretation [25]:

POL(0) = 0
POL(AND(x₁, x₂)) = x₂
POL(ISNATILISTKIND(x₁)) = x₁
POL(ISNATKIND(x₁)) = 2·x₁
POL(U(x₁)) = x₁
POL(U11(x₁, x₂)) = 0
POL(U12(x₁)) = 2·x₁
POL(U21(x₁, x₂)) = 0
POL(U22(x₁)) = x₁
POL(U51(x₁, x₂, x₃)) = 0
POL(U52(x₁, x₂)) = 0
POL(U53(x₁)) = 2·x₁
POL(U61(x₁, x₂)) = 2 + x₁ + 2·x₂
POL(and(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = 2·x₁ + 2·x₂
POL(isNat(x₁)) = 0
POL(isNatIListKind(x₁)) = 2·x₁
POL(isNatKind(x₁)) = x₁
POL(isNatList(x₁)) = 0
POL(length(x₁)) = 2 + 2·x₁
POL(nil) = 0
POL(s(x₁)) = x₁
POL(tt) = 0
POL(zeros) = 0

the following usable rules

and(tt, X) → X
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → and(isNatKind(V1), isNatIListKind(V2))
zeros → cons(0, zeros)
isNatKind(0) → tt
isNatKind(length(V1)) → isNatIListKind(V1)
isNatKind(s(V1)) → isNatKind(V1)
length(nil) → 0
length(cons(N, L)) → U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)
U61(tt, L) → s(length(L))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
U51(tt, V1, V2) → U52(isNat(V1), V2)
U52(tt, V2) → U53(isNatList(V2))
U53(tt) → tt
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
U11(tt, V1) → U12(isNatList(V1))
U12(tt) → tt
U21(tt, V1) → U22(isNat(V1))
U22(tt) → tt

could all be oriented weakly.
Furthermore, the pairs

ISNATKIND(length(V1)) → ISNATILISTKIND(V1)

could be oriented strictly and thus removed.
The pairs

AND(tt, X) → U(X)
U(and(x_0, x_1)) → U(x_0)
U(isNatIListKind(V2)) → ISNATILISTKIND(V2)
ISNATILISTKIND(cons(V1, V2)) → AND(isNatKind(V1), isNatIListKind(V2))
ISNATILISTKIND(cons(V1, V2)) → ISNATKIND(V1)
ISNATKIND(s(V1)) → ISNATKIND(V1)

could only be oriented weakly and must be analyzed further.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

          ↳ QCSDP

          ↳ QCSDP

          ↳ QCSDP

  ↳ Incomplete Giesl Middeldorp-Transformation

AND(tt, X) → U(X)
U(and(x_0, x_1)) → U(x_0)
U(isNatIListKind(V2)) → ISNATILISTKIND(V2)
ISNATILISTKIND(cons(V1, V2)) → AND(isNatKind(V1), isNatIListKind(V2))
ISNATILISTKIND(cons(V1, V2)) → ISNATKIND(V1)
ISNATKIND(s(V1)) → ISNATKIND(V1)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, V1) → U12(isNatList(V1))
U12(tt) → tt
U21(tt, V1) → U22(isNat(V1))
U22(tt) → tt
U31(tt, V) → U32(isNatList(V))
U32(tt) → tt
U41(tt, V1, V2) → U42(isNat(V1), V2)
U42(tt, V2) → U43(isNatIList(V2))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNat(V1), V2)
U52(tt, V2) → U53(isNatList(V2))
U53(tt) → tt
U61(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
isNatIList(V) → U31(isNatIListKind(V), V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → and(isNatKind(V1), isNatIListKind(V2))
isNatKind(0) → tt
isNatKind(length(V1)) → isNatIListKind(V1)
isNatKind(s(V1)) → isNatKind(V1)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
length(nil) → 0
length(cons(N, L)) → U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 2 SCCs with 1 less node.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

                  ↳ AND

                    ↳ QCSDP

                      ↳ QCSDPSubtermProof

                    ↳ QCSDP

          ↳ QCSDP

          ↳ QCSDP

          ↳ QCSDP

  ↳ Incomplete Giesl Middeldorp-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {U12, U22, U32, U43, U53, s, length} are replacing on all positions.
For all symbols f in {cons, U11, U21, U31, U41, U42, U51, U52, U61, and} we have µ(f) = {1}.
The symbols in {isNatList, isNat, isNatIList, isNatIListKind, isNatKind, ISNATKIND} are not replacing on any position.

The TRS P consists of the following rules:

ISNATKIND(s(V1)) → ISNATKIND(V1)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, V1) → U12(isNatList(V1))
U12(tt) → tt
U21(tt, V1) → U22(isNat(V1))
U22(tt) → tt
U31(tt, V) → U32(isNatList(V))
U32(tt) → tt
U41(tt, V1, V2) → U42(isNat(V1), V2)
U42(tt, V2) → U43(isNatIList(V2))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNat(V1), V2)
U52(tt, V2) → U53(isNatList(V2))
U53(tt) → tt
U61(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
isNatIList(V) → U31(isNatIListKind(V), V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → and(isNatKind(V1), isNatIListKind(V2))
isNatKind(0) → tt
isNatKind(length(V1)) → isNatIListKind(V1)
isNatKind(s(V1)) → isNatKind(V1)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
length(nil) → 0
length(cons(N, L)) → U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

Q is empty.

We use the subterm processor [20].

The following pairs can be oriented strictly and are deleted.

ISNATKIND(s(V1)) → ISNATKIND(V1)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
ISNATKIND(x1) = x1

Subterm Order

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

                  ↳ AND

                    ↳ QCSDP

                      ↳ QCSDPSubtermProof

                        ↳ QCSDP

                          ↳ PIsEmptyProof

                    ↳ QCSDP

          ↳ QCSDP

          ↳ QCSDP

          ↳ QCSDP

  ↳ Incomplete Giesl Middeldorp-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {U12, U22, U32, U43, U53, s, length} are replacing on all positions.
For all symbols f in {cons, U11, U21, U31, U41, U42, U51, U52, U61, and} we have µ(f) = {1}.
The symbols in {isNatList, isNat, isNatIList, isNatIListKind, isNatKind} are not replacing on any position.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, V1) → U12(isNatList(V1))
U12(tt) → tt
U21(tt, V1) → U22(isNat(V1))
U22(tt) → tt
U31(tt, V) → U32(isNatList(V))
U32(tt) → tt
U41(tt, V1, V2) → U42(isNat(V1), V2)
U42(tt, V2) → U43(isNatIList(V2))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNat(V1), V2)
U52(tt, V2) → U53(isNatList(V2))
U53(tt) → tt
U61(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
isNatIList(V) → U31(isNatIListKind(V), V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → and(isNatKind(V1), isNatIListKind(V2))
isNatKind(0) → tt
isNatKind(length(V1)) → isNatIListKind(V1)
isNatKind(s(V1)) → isNatKind(V1)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
length(nil) → 0
length(cons(N, L)) → U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

Q is empty.

The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

                  ↳ AND

                    ↳ QCSDP

                    ↳ QCSDP

                      ↳ QCSDPNarrowingProcessor

          ↳ QCSDP

          ↳ QCSDP

          ↳ QCSDP

  ↳ Incomplete Giesl Middeldorp-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {U12, U22, U32, U43, U53, s, length} are replacing on all positions.
For all symbols f in {cons, U11, U21, U31, U41, U42, U51, U52, U61, and, AND} we have µ(f) = {1}.
The symbols in {isNatList, isNat, isNatIList, isNatIListKind, isNatKind, U, ISNATILISTKIND} are not replacing on any position.

The TRS P consists of the following rules:

U(and(x_0, x_1)) → U(x_0)
U(isNatIListKind(V2)) → ISNATILISTKIND(V2)
ISNATILISTKIND(cons(V1, V2)) → AND(isNatKind(V1), isNatIListKind(V2))
AND(tt, X) → U(X)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, V1) → U12(isNatList(V1))
U12(tt) → tt
U21(tt, V1) → U22(isNat(V1))
U22(tt) → tt
U31(tt, V) → U32(isNatList(V))
U32(tt) → tt
U41(tt, V1, V2) → U42(isNat(V1), V2)
U42(tt, V2) → U43(isNatIList(V2))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNat(V1), V2)
U52(tt, V2) → U53(isNatList(V2))
U53(tt) → tt
U61(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
isNatIList(V) → U31(isNatIListKind(V), V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → and(isNatKind(V1), isNatIListKind(V2))
isNatKind(0) → tt
isNatKind(length(V1)) → isNatIListKind(V1)
isNatKind(s(V1)) → isNatKind(V1)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
length(nil) → 0
length(cons(N, L)) → U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

Q is empty.

Using the Context-Sensitive Narrowing Processor
the pair ISNATILISTKIND(cons(V1, V2)) → AND(isNatKind(V1), isNatIListKind(V2))
was transformed to the following new pairs:

ISNATILISTKIND(cons(0, y1)) → AND(tt, isNatIListKind(y1))
ISNATILISTKIND(cons(length(x0), y1)) → AND(isNatIListKind(x0), isNatIListKind(y1))
ISNATILISTKIND(cons(s(x0), y1)) → AND(isNatKind(x0), isNatIListKind(y1))

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

                  ↳ AND

                    ↳ QCSDP

                    ↳ QCSDP

                      ↳ QCSDPNarrowingProcessor

                        ↳ QCSDP

                          ↳ QCSDPReductionPairProof

          ↳ QCSDP

          ↳ QCSDP

          ↳ QCSDP

  ↳ Incomplete Giesl Middeldorp-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {U12, U22, U32, U43, U53, s, length} are replacing on all positions.
For all symbols f in {cons, U11, U21, U31, U41, U42, U51, U52, U61, and, AND} we have µ(f) = {1}.
The symbols in {isNatList, isNat, isNatIList, isNatIListKind, isNatKind, U, ISNATILISTKIND} are not replacing on any position.

The TRS P consists of the following rules:

U(and(x_0, x_1)) → U(x_0)
U(isNatIListKind(V2)) → ISNATILISTKIND(V2)
AND(tt, X) → U(X)
ISNATILISTKIND(cons(s(x0), y1)) → AND(isNatKind(x0), isNatIListKind(y1))
ISNATILISTKIND(cons(0, y1)) → AND(tt, isNatIListKind(y1))
ISNATILISTKIND(cons(length(x0), y1)) → AND(isNatIListKind(x0), isNatIListKind(y1))

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, V1) → U12(isNatList(V1))
U12(tt) → tt
U21(tt, V1) → U22(isNat(V1))
U22(tt) → tt
U31(tt, V) → U32(isNatList(V))
U32(tt) → tt
U41(tt, V1, V2) → U42(isNat(V1), V2)
U42(tt, V2) → U43(isNatIList(V2))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNat(V1), V2)
U52(tt, V2) → U53(isNatList(V2))
U53(tt) → tt
U61(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
isNatIList(V) → U31(isNatIListKind(V), V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → and(isNatKind(V1), isNatIListKind(V2))
isNatKind(0) → tt
isNatKind(length(V1)) → isNatIListKind(V1)
isNatKind(s(V1)) → isNatKind(V1)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
length(nil) → 0
length(cons(N, L)) → U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

Q is empty.

Using the order
Polynomial interpretation [25]:

POL(0) = 0
POL(AND(x₁, x₂)) = 2·x₂
POL(ISNATILISTKIND(x₁)) = x₁
POL(U(x₁)) = 2·x₁
POL(U11(x₁, x₂)) = 0
POL(U12(x₁)) = 0
POL(U21(x₁, x₂)) = 0
POL(U22(x₁)) = 0
POL(U51(x₁, x₂, x₃)) = x₁ + 2·x₂ + 2·x₃
POL(U52(x₁, x₂)) = x₂
POL(U53(x₁)) = 0
POL(U61(x₁, x₂)) = 2 + x₂
POL(and(x₁, x₂)) = 2·x₁ + 2·x₂
POL(cons(x₁, x₂)) = 2·x₁ + 2·x₂
POL(isNat(x₁)) = 0
POL(isNatIListKind(x₁)) = x₁
POL(isNatKind(x₁)) = x₁
POL(isNatList(x₁)) = 2·x₁
POL(length(x₁)) = 2 + x₁
POL(nil) = 2
POL(s(x₁)) = x₁
POL(tt) = 0
POL(zeros) = 0

the following usable rules

and(tt, X) → X
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → and(isNatKind(V1), isNatIListKind(V2))
zeros → cons(0, zeros)
isNatKind(0) → tt
isNatKind(length(V1)) → isNatIListKind(V1)
isNatKind(s(V1)) → isNatKind(V1)
length(nil) → 0
length(cons(N, L)) → U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)
U61(tt, L) → s(length(L))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
U51(tt, V1, V2) → U52(isNat(V1), V2)
U52(tt, V2) → U53(isNatList(V2))
U53(tt) → tt
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
U11(tt, V1) → U12(isNatList(V1))
U12(tt) → tt
U21(tt, V1) → U22(isNat(V1))
U22(tt) → tt

could all be oriented weakly.
Furthermore, the pairs

ISNATILISTKIND(cons(length(x0), y1)) → AND(isNatIListKind(x0), isNatIListKind(y1))

could be oriented strictly and thus removed.
The pairs

U(and(x_0, x_1)) → U(x_0)
U(isNatIListKind(V2)) → ISNATILISTKIND(V2)
AND(tt, X) → U(X)
ISNATILISTKIND(cons(s(x0), y1)) → AND(isNatKind(x0), isNatIListKind(y1))
ISNATILISTKIND(cons(0, y1)) → AND(tt, isNatIListKind(y1))

could only be oriented weakly and must be analyzed further.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

                  ↳ AND

                    ↳ QCSDP

                    ↳ QCSDP

                      ↳ QCSDPNarrowingProcessor

                        ↳ QCSDP

                          ↳ QCSDPReductionPairProof

                            ↳ QCSDP

                              ↳ QCSDPNarrowingProcessor

          ↳ QCSDP

          ↳ QCSDP

          ↳ QCSDP

  ↳ Incomplete Giesl Middeldorp-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {U12, U22, U32, U43, U53, s, length} are replacing on all positions.
For all symbols f in {cons, U11, U21, U31, U41, U42, U51, U52, U61, and, AND} we have µ(f) = {1}.
The symbols in {isNatList, isNat, isNatIList, isNatIListKind, isNatKind, U, ISNATILISTKIND} are not replacing on any position.

The TRS P consists of the following rules:

U(and(x_0, x_1)) → U(x_0)
U(isNatIListKind(V2)) → ISNATILISTKIND(V2)
AND(tt, X) → U(X)
ISNATILISTKIND(cons(s(x0), y1)) → AND(isNatKind(x0), isNatIListKind(y1))
ISNATILISTKIND(cons(0, y1)) → AND(tt, isNatIListKind(y1))

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, V1) → U12(isNatList(V1))
U12(tt) → tt
U21(tt, V1) → U22(isNat(V1))
U22(tt) → tt
U31(tt, V) → U32(isNatList(V))
U32(tt) → tt
U41(tt, V1, V2) → U42(isNat(V1), V2)
U42(tt, V2) → U43(isNatIList(V2))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNat(V1), V2)
U52(tt, V2) → U53(isNatList(V2))
U53(tt) → tt
U61(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
isNatIList(V) → U31(isNatIListKind(V), V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → and(isNatKind(V1), isNatIListKind(V2))
isNatKind(0) → tt
isNatKind(length(V1)) → isNatIListKind(V1)
isNatKind(s(V1)) → isNatKind(V1)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
length(nil) → 0
length(cons(N, L)) → U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

Q is empty.

Using the Context-Sensitive Narrowing Processor
the pair ISNATILISTKIND(cons(s(x0), y1)) → AND(isNatKind(x0), isNatIListKind(y1))
was transformed to the following new pairs:

ISNATILISTKIND(cons(s(0), y1)) → AND(tt, isNatIListKind(y1))
ISNATILISTKIND(cons(s(length(x0)), y1)) → AND(isNatIListKind(x0), isNatIListKind(y1))
ISNATILISTKIND(cons(s(s(x0)), y1)) → AND(isNatKind(x0), isNatIListKind(y1))

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

                  ↳ AND

                    ↳ QCSDP

                    ↳ QCSDP

                      ↳ QCSDPNarrowingProcessor

                        ↳ QCSDP

                          ↳ QCSDPReductionPairProof

                            ↳ QCSDP

                              ↳ QCSDPNarrowingProcessor

                                ↳ QCSDP

                                  ↳ QCSDPReductionPairProof

          ↳ QCSDP

          ↳ QCSDP

          ↳ QCSDP

  ↳ Incomplete Giesl Middeldorp-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {U12, U22, U32, U43, U53, s, length} are replacing on all positions.
For all symbols f in {cons, U11, U21, U31, U41, U42, U51, U52, U61, and, AND} we have µ(f) = {1}.
The symbols in {isNatList, isNat, isNatIList, isNatIListKind, isNatKind, U, ISNATILISTKIND} are not replacing on any position.

The TRS P consists of the following rules:

U(and(x_0, x_1)) → U(x_0)
U(isNatIListKind(V2)) → ISNATILISTKIND(V2)
ISNATILISTKIND(cons(s(length(x0)), y1)) → AND(isNatIListKind(x0), isNatIListKind(y1))
ISNATILISTKIND(cons(s(0), y1)) → AND(tt, isNatIListKind(y1))
AND(tt, X) → U(X)
ISNATILISTKIND(cons(s(s(x0)), y1)) → AND(isNatKind(x0), isNatIListKind(y1))
ISNATILISTKIND(cons(0, y1)) → AND(tt, isNatIListKind(y1))

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, V1) → U12(isNatList(V1))
U12(tt) → tt
U21(tt, V1) → U22(isNat(V1))
U22(tt) → tt
U31(tt, V) → U32(isNatList(V))
U32(tt) → tt
U41(tt, V1, V2) → U42(isNat(V1), V2)
U42(tt, V2) → U43(isNatIList(V2))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNat(V1), V2)
U52(tt, V2) → U53(isNatList(V2))
U53(tt) → tt
U61(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
isNatIList(V) → U31(isNatIListKind(V), V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → and(isNatKind(V1), isNatIListKind(V2))
isNatKind(0) → tt
isNatKind(length(V1)) → isNatIListKind(V1)
isNatKind(s(V1)) → isNatKind(V1)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
length(nil) → 0
length(cons(N, L)) → U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

Q is empty.

Using the order
Polynomial interpretation [25]:

POL(0) = 0
POL(AND(x₁, x₂)) = x₂
POL(ISNATILISTKIND(x₁)) = 2·x₁
POL(U(x₁)) = x₁
POL(U11(x₁, x₂)) = 1 + x₂
POL(U12(x₁)) = 1
POL(U21(x₁, x₂)) = x₁
POL(U22(x₁)) = 0
POL(U51(x₁, x₂, x₃)) = 0
POL(U52(x₁, x₂)) = 0
POL(U53(x₁)) = 0
POL(U61(x₁, x₂)) = 2 + 2·x₂
POL(and(x₁, x₂)) = 2·x₁ + x₂
POL(cons(x₁, x₂)) = x₁ + x₂
POL(isNat(x₁)) = 2·x₁
POL(isNatIListKind(x₁)) = 2·x₁
POL(isNatKind(x₁)) = x₁
POL(isNatList(x₁)) = 2
POL(length(x₁)) = 2 + 2·x₁
POL(nil) = 0
POL(s(x₁)) = x₁
POL(tt) = 0
POL(zeros) = 0

the following usable rules

and(tt, X) → X
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → and(isNatKind(V1), isNatIListKind(V2))
zeros → cons(0, zeros)
isNatKind(0) → tt
isNatKind(length(V1)) → isNatIListKind(V1)
isNatKind(s(V1)) → isNatKind(V1)
length(nil) → 0
length(cons(N, L)) → U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)
U61(tt, L) → s(length(L))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
U51(tt, V1, V2) → U52(isNat(V1), V2)
U52(tt, V2) → U53(isNatList(V2))
U53(tt) → tt
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
U11(tt, V1) → U12(isNatList(V1))
U12(tt) → tt
U21(tt, V1) → U22(isNat(V1))
U22(tt) → tt

could all be oriented weakly.
Furthermore, the pairs

ISNATILISTKIND(cons(s(length(x0)), y1)) → AND(isNatIListKind(x0), isNatIListKind(y1))

could be oriented strictly and thus removed.
The pairs

U(and(x_0, x_1)) → U(x_0)
U(isNatIListKind(V2)) → ISNATILISTKIND(V2)
ISNATILISTKIND(cons(s(0), y1)) → AND(tt, isNatIListKind(y1))
AND(tt, X) → U(X)
ISNATILISTKIND(cons(s(s(x0)), y1)) → AND(isNatKind(x0), isNatIListKind(y1))
ISNATILISTKIND(cons(0, y1)) → AND(tt, isNatIListKind(y1))

could only be oriented weakly and must be analyzed further.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

                  ↳ AND

                    ↳ QCSDP

                    ↳ QCSDP

                      ↳ QCSDPNarrowingProcessor

                        ↳ QCSDP

                          ↳ QCSDPReductionPairProof

                            ↳ QCSDP

                              ↳ QCSDPNarrowingProcessor

                                ↳ QCSDP

                                  ↳ QCSDPReductionPairProof

                                    ↳ QCSDP

                                      ↳ QCSDPNarrowingProcessor

          ↳ QCSDP

          ↳ QCSDP

          ↳ QCSDP

  ↳ Incomplete Giesl Middeldorp-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {U12, U22, U32, U43, U53, s, length} are replacing on all positions.
For all symbols f in {cons, U11, U21, U31, U41, U42, U51, U52, U61, and, AND} we have µ(f) = {1}.
The symbols in {isNatList, isNat, isNatIList, isNatIListKind, isNatKind, U, ISNATILISTKIND} are not replacing on any position.

The TRS P consists of the following rules:

U(and(x_0, x_1)) → U(x_0)
U(isNatIListKind(V2)) → ISNATILISTKIND(V2)
ISNATILISTKIND(cons(s(0), y1)) → AND(tt, isNatIListKind(y1))
AND(tt, X) → U(X)
ISNATILISTKIND(cons(s(s(x0)), y1)) → AND(isNatKind(x0), isNatIListKind(y1))
ISNATILISTKIND(cons(0, y1)) → AND(tt, isNatIListKind(y1))

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, V1) → U12(isNatList(V1))
U12(tt) → tt
U21(tt, V1) → U22(isNat(V1))
U22(tt) → tt
U31(tt, V) → U32(isNatList(V))
U32(tt) → tt
U41(tt, V1, V2) → U42(isNat(V1), V2)
U42(tt, V2) → U43(isNatIList(V2))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNat(V1), V2)
U52(tt, V2) → U53(isNatList(V2))
U53(tt) → tt
U61(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
isNatIList(V) → U31(isNatIListKind(V), V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → and(isNatKind(V1), isNatIListKind(V2))
isNatKind(0) → tt
isNatKind(length(V1)) → isNatIListKind(V1)
isNatKind(s(V1)) → isNatKind(V1)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
length(nil) → 0
length(cons(N, L)) → U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

Q is empty.

Using the Context-Sensitive Narrowing Processor
the pair ISNATILISTKIND(cons(s(s(x0)), y1)) → AND(isNatKind(x0), isNatIListKind(y1))
was transformed to the following new pairs:

ISNATILISTKIND(cons(s(s(0)), y1)) → AND(tt, isNatIListKind(y1))
ISNATILISTKIND(cons(s(s(length(x0))), y1)) → AND(isNatIListKind(x0), isNatIListKind(y1))
ISNATILISTKIND(cons(s(s(s(x0))), y1)) → AND(isNatKind(x0), isNatIListKind(y1))

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPReductionPairProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

                  ↳ AND

                    ↳ QCSDP

                    ↳ QCSDP

                      ↳ QCSDPNarrowingProcessor

                        ↳ QCSDP

                          ↳ QCSDPReductionPairProof

                            ↳ QCSDP

                              ↳ QCSDPNarrowingProcessor

                                ↳ QCSDP

                                  ↳ QCSDPReductionPairProof

                                    ↳ QCSDP

                                      ↳ QCSDPNarrowingProcessor

                                        ↳ QCSDP

          ↳ QCSDP

          ↳ QCSDP

          ↳ QCSDP

  ↳ Incomplete Giesl Middeldorp-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {U12, U22, U32, U43, U53, s, length} are replacing on all positions.
For all symbols f in {cons, U11, U21, U31, U41, U42, U51, U52, U61, and, AND} we have µ(f) = {1}.
The symbols in {isNatList, isNat, isNatIList, isNatIListKind, isNatKind, U, ISNATILISTKIND} are not replacing on any position.

The TRS P consists of the following rules:

U(and(x_0, x_1)) → U(x_0)
U(isNatIListKind(V2)) → ISNATILISTKIND(V2)
ISNATILISTKIND(cons(s(0), y1)) → AND(tt, isNatIListKind(y1))
AND(tt, X) → U(X)
ISNATILISTKIND(cons(s(s(0)), y1)) → AND(tt, isNatIListKind(y1))
ISNATILISTKIND(cons(s(s(length(x0))), y1)) → AND(isNatIListKind(x0), isNatIListKind(y1))
ISNATILISTKIND(cons(s(s(s(x0))), y1)) → AND(isNatKind(x0), isNatIListKind(y1))
ISNATILISTKIND(cons(0, y1)) → AND(tt, isNatIListKind(y1))

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, V1) → U12(isNatList(V1))
U12(tt) → tt
U21(tt, V1) → U22(isNat(V1))
U22(tt) → tt
U31(tt, V) → U32(isNatList(V))
U32(tt) → tt
U41(tt, V1, V2) → U42(isNat(V1), V2)
U42(tt, V2) → U43(isNatIList(V2))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNat(V1), V2)
U52(tt, V2) → U53(isNatList(V2))
U53(tt) → tt
U61(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
isNatIList(V) → U31(isNatIListKind(V), V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → and(isNatKind(V1), isNatIListKind(V2))
isNatKind(0) → tt
isNatKind(length(V1)) → isNatIListKind(V1)
isNatKind(s(V1)) → isNatKind(V1)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
length(nil) → 0
length(cons(N, L)) → U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

Q is empty.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

          ↳ QCSDP

          ↳ QCSDP

          ↳ QCSDP

  ↳ Incomplete Giesl Middeldorp-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {U12, U22, U32, U43, U53, s, length} are replacing on all positions.
For all symbols f in {cons, U11, U21, U31, U41, U42, U51, U52, U61, and, U51¹, U52¹, U11¹, U21¹} we have µ(f) = {1}.
The symbols in {isNatList, isNat, isNatIList, isNatIListKind, isNatKind, ISNATLIST, ISNAT} are not replacing on any position.

The TRS P consists of the following rules:

ISNATLIST(cons(V1, V2)) → U51¹(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
U51¹(tt, V1, V2) → U52¹(isNat(V1), V2)
U52¹(tt, V2) → ISNATLIST(V2)
U51¹(tt, V1, V2) → ISNAT(V1)
ISNAT(length(V1)) → U11¹(isNatIListKind(V1), V1)
U11¹(tt, V1) → ISNATLIST(V1)
ISNAT(s(V1)) → U21¹(isNatKind(V1), V1)
U21¹(tt, V1) → ISNAT(V1)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, V1) → U12(isNatList(V1))
U12(tt) → tt
U21(tt, V1) → U22(isNat(V1))
U22(tt) → tt
U31(tt, V) → U32(isNatList(V))
U32(tt) → tt
U41(tt, V1, V2) → U42(isNat(V1), V2)
U42(tt, V2) → U43(isNatIList(V2))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNat(V1), V2)
U52(tt, V2) → U53(isNatList(V2))
U53(tt) → tt
U61(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
isNatIList(V) → U31(isNatIListKind(V), V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → and(isNatKind(V1), isNatIListKind(V2))
isNatKind(0) → tt
isNatKind(length(V1)) → isNatIListKind(V1)
isNatKind(s(V1)) → isNatKind(V1)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
length(nil) → 0
length(cons(N, L)) → U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

Q is empty.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

          ↳ QCSDP

          ↳ QCSDP

          ↳ QCSDP

  ↳ Incomplete Giesl Middeldorp-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {U12, U22, U32, U43, U53, s, length, LENGTH} are replacing on all positions.
For all symbols f in {cons, U11, U21, U31, U41, U42, U51, U52, U61, and, U61¹} we have µ(f) = {1}.
The symbols in {isNatList, isNat, isNatIList, isNatIListKind, isNatKind} are not replacing on any position.

The TRS P consists of the following rules:

LENGTH(cons(N, L)) → U61¹(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)
U61¹(tt, L) → LENGTH(L)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, V1) → U12(isNatList(V1))
U12(tt) → tt
U21(tt, V1) → U22(isNat(V1))
U22(tt) → tt
U31(tt, V) → U32(isNatList(V))
U32(tt) → tt
U41(tt, V1, V2) → U42(isNat(V1), V2)
U42(tt, V2) → U43(isNatIList(V2))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNat(V1), V2)
U52(tt, V2) → U53(isNatList(V2))
U53(tt) → tt
U61(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
isNatIList(V) → U31(isNatIListKind(V), V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → and(isNatKind(V1), isNatIListKind(V2))
isNatKind(0) → tt
isNatKind(length(V1)) → isNatIListKind(V1)
isNatKind(s(V1)) → isNatKind(V1)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
length(nil) → 0
length(cons(N, L)) → U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

Q is empty.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

          ↳ QCSDP

          ↳ QCSDP

          ↳ QCSDP

  ↳ Incomplete Giesl Middeldorp-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {U12, U22, U32, U43, U53, s, length} are replacing on all positions.
For all symbols f in {cons, U11, U21, U31, U41, U42, U51, U52, U61, and, U42¹, U41¹} we have µ(f) = {1}.
The symbols in {isNatList, isNat, isNatIList, isNatIListKind, isNatKind, ISNATILIST} are not replacing on any position.

The TRS P consists of the following rules:

U41¹(tt, V1, V2) → U42¹(isNat(V1), V2)
U42¹(tt, V2) → ISNATILIST(V2)
ISNATILIST(cons(V1, V2)) → U41¹(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, V1) → U12(isNatList(V1))
U12(tt) → tt
U21(tt, V1) → U22(isNat(V1))
U22(tt) → tt
U31(tt, V) → U32(isNatList(V))
U32(tt) → tt
U41(tt, V1, V2) → U42(isNat(V1), V2)
U42(tt, V2) → U43(isNatIList(V2))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNat(V1), V2)
U52(tt, V2) → U53(isNatList(V2))
U53(tt) → tt
U61(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → U11(isNatIListKind(V1), V1)
isNat(s(V1)) → U21(isNatKind(V1), V1)
isNatIList(V) → U31(isNatIListKind(V), V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
isNatIListKind(nil) → tt
isNatIListKind(zeros) → tt
isNatIListKind(cons(V1, V2)) → and(isNatKind(V1), isNatIListKind(V2))
isNatKind(0) → tt
isNatKind(length(V1)) → isNatIListKind(V1)
isNatKind(s(V1)) → isNatKind(V1)
isNatList(nil) → tt
isNatList(cons(V1, V2)) → U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
length(nil) → 0
length(cons(N, L)) → U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

Q is empty.

We applied the Incomplete Giesl Middeldorp transformation [11] to transform the context-sensitive TRS to a usual TRS.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U12(x1)) → U12Active(mark(x1))
U12Active(x1) → U12(x1)
mark(U21(x1, x2)) → U21Active(mark(x1), x2)
U21Active(x1, x2) → U21(x1, x2)
mark(U22(x1)) → U22Active(mark(x1))
U22Active(x1) → U22(x1)
mark(U31(x1, x2)) → U31Active(mark(x1), x2)
U31Active(x1, x2) → U31(x1, x2)
mark(U32(x1)) → U32Active(mark(x1))
U32Active(x1) → U32(x1)
mark(U41(x1, x2, x3)) → U41Active(mark(x1), x2, x3)
U41Active(x1, x2, x3) → U41(x1, x2, x3)
mark(U42(x1, x2)) → U42Active(mark(x1), x2)
U42Active(x1, x2) → U42(x1, x2)
mark(U43(x1)) → U43Active(mark(x1))
U43Active(x1) → U43(x1)
mark(U51(x1, x2, x3)) → U51Active(mark(x1), x2, x3)
U51Active(x1, x2, x3) → U51(x1, x2, x3)
mark(U52(x1, x2)) → U52Active(mark(x1), x2)
U52Active(x1, x2) → U52(x1, x2)
mark(U53(x1)) → U53Active(mark(x1))
U53Active(x1) → U53(x1)
mark(U61(x1, x2)) → U61Active(mark(x1), x2)
U61Active(x1, x2) → U61(x1, x2)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatIListKind(x1)) → isNatIListKindActive(x1)
isNatIListKindActive(x1) → isNatIListKind(x1)
mark(isNatKind(x1)) → isNatKindActive(x1)
isNatKindActive(x1) → isNatKind(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, V1) → U12Active(isNatListActive(V1))
U12Active(tt) → tt
U21Active(tt, V1) → U22Active(isNatActive(V1))
U22Active(tt) → tt
U31Active(tt, V) → U32Active(isNatListActive(V))
U32Active(tt) → tt
U41Active(tt, V1, V2) → U42Active(isNatActive(V1), V2)
U42Active(tt, V2) → U43Active(isNatIListActive(V2))
U43Active(tt) → tt
U51Active(tt, V1, V2) → U52Active(isNatActive(V1), V2)
U52Active(tt, V2) → U53Active(isNatListActive(V2))
U53Active(tt) → tt
U61Active(tt, L) → s(lengthActive(mark(L)))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → U11Active(isNatIListKindActive(V1), V1)
isNatActive(s(V1)) → U21Active(isNatKindActive(V1), V1)
isNatIListActive(V) → U31Active(isNatIListKindActive(V), V)
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → U41Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
isNatIListKindActive(nil) → tt
isNatIListKindActive(zeros) → tt
isNatIListKindActive(cons(V1, V2)) → andActive(isNatKindActive(V1), isNatIListKind(V2))
isNatKindActive(0) → tt
isNatKindActive(length(V1)) → isNatIListKindActive(V1)
isNatKindActive(s(V1)) → isNatKindActive(V1)
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → U51Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U61Active(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

MARK(U11(x1, x2)) → MARK(x1)
U11ACTIVE(tt, V1) → U12ACTIVE(isNatListActive(V1))
MARK(isNatKind(x1)) → ISNATKINDACTIVE(x1)
MARK(U42(x1, x2)) → U42ACTIVE(mark(x1), x2)
MARK(cons(x1, x2)) → MARK(x1)
U51ACTIVE(tt, V1, V2) → U52ACTIVE(isNatActive(V1), V2)
U51ACTIVE(tt, V1, V2) → ISNATACTIVE(V1)
MARK(U12(x1)) → U12ACTIVE(mark(x1))
MARK(and(x1, x2)) → ANDACTIVE(mark(x1), x2)
MARK(length(x1)) → MARK(x1)
ISNATILISTKINDACTIVE(cons(V1, V2)) → ANDACTIVE(isNatKindActive(V1), isNatIListKind(V2))
MARK(U32(x1)) → U32ACTIVE(mark(x1))
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
ISNATLISTACTIVE(cons(V1, V2)) → ISNATKINDACTIVE(V1)
MARK(U51(x1, x2, x3)) → MARK(x1)
MARK(U53(x1)) → U53ACTIVE(mark(x1))
MARK(U53(x1)) → MARK(x1)
ISNATILISTACTIVE(V) → ISNATILISTKINDACTIVE(V)
ISNATILISTACTIVE(cons(V1, V2)) → U41ACTIVE(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
MARK(U41(x1, x2, x3)) → MARK(x1)
ISNATACTIVE(s(V1)) → U21ACTIVE(isNatKindActive(V1), V1)
MARK(U11(x1, x2)) → U11ACTIVE(mark(x1), x2)
ISNATKINDACTIVE(s(V1)) → ISNATKINDACTIVE(V1)
U61ACTIVE(tt, L) → LENGTHACTIVE(mark(L))
MARK(U43(x1)) → U43ACTIVE(mark(x1))
LENGTHACTIVE(cons(N, L)) → U61ACTIVE(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)
MARK(U32(x1)) → MARK(x1)
MARK(U22(x1)) → MARK(x1)
LENGTHACTIVE(cons(N, L)) → ANDACTIVE(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N)))
ISNATACTIVE(s(V1)) → ISNATKINDACTIVE(V1)
LENGTHACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
MARK(U51(x1, x2, x3)) → U51ACTIVE(mark(x1), x2, x3)
U21ACTIVE(tt, V1) → U22ACTIVE(isNatActive(V1))
U61ACTIVE(tt, L) → MARK(L)
MARK(U21(x1, x2)) → MARK(x1)
U41ACTIVE(tt, V1, V2) → ISNATACTIVE(V1)
MARK(U42(x1, x2)) → MARK(x1)
U41ACTIVE(tt, V1, V2) → U42ACTIVE(isNatActive(V1), V2)
MARK(U52(x1, x2)) → MARK(x1)
MARK(U12(x1)) → MARK(x1)
MARK(length(x1)) → LENGTHACTIVE(mark(x1))
ISNATACTIVE(length(V1)) → ISNATILISTKINDACTIVE(V1)
MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(s(x1)) → MARK(x1)
ISNATLISTACTIVE(cons(V1, V2)) → U51ACTIVE(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
MARK(U31(x1, x2)) → MARK(x1)
U11ACTIVE(tt, V1) → ISNATLISTACTIVE(V1)
ISNATILISTKINDACTIVE(cons(V1, V2)) → ISNATKINDACTIVE(V1)
MARK(zeros) → ZEROSACTIVE
ISNATACTIVE(length(V1)) → U11ACTIVE(isNatIListKindActive(V1), V1)
ANDACTIVE(tt, X) → MARK(X)
MARK(U52(x1, x2)) → U52ACTIVE(mark(x1), x2)
LENGTHACTIVE(cons(N, L)) → ANDACTIVE(isNatListActive(L), isNatIListKind(L))
MARK(and(x1, x2)) → MARK(x1)
MARK(U61(x1, x2)) → U61ACTIVE(mark(x1), x2)
MARK(isNat(x1)) → ISNATACTIVE(x1)
MARK(U41(x1, x2, x3)) → U41ACTIVE(mark(x1), x2, x3)
ISNATKINDACTIVE(length(V1)) → ISNATILISTKINDACTIVE(V1)
MARK(U21(x1, x2)) → U21ACTIVE(mark(x1), x2)
ISNATILISTACTIVE(V) → U31ACTIVE(isNatIListKindActive(V), V)
U42ACTIVE(tt, V2) → U43ACTIVE(isNatIListActive(V2))
MARK(U22(x1)) → U22ACTIVE(mark(x1))
MARK(U61(x1, x2)) → MARK(x1)
MARK(U43(x1)) → MARK(x1)
U21ACTIVE(tt, V1) → ISNATACTIVE(V1)
U31ACTIVE(tt, V) → ISNATLISTACTIVE(V)
ISNATILISTACTIVE(cons(V1, V2)) → ISNATKINDACTIVE(V1)
U31ACTIVE(tt, V) → U32ACTIVE(isNatListActive(V))
ISNATILISTACTIVE(cons(V1, V2)) → ANDACTIVE(isNatKindActive(V1), isNatIListKind(V2))
U52ACTIVE(tt, V2) → U53ACTIVE(isNatListActive(V2))
ISNATLISTACTIVE(cons(V1, V2)) → ANDACTIVE(isNatKindActive(V1), isNatIListKind(V2))
MARK(U31(x1, x2)) → U31ACTIVE(mark(x1), x2)
U42ACTIVE(tt, V2) → ISNATILISTACTIVE(V2)
U52ACTIVE(tt, V2) → ISNATLISTACTIVE(V2)
MARK(isNatIListKind(x1)) → ISNATILISTKINDACTIVE(x1)

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U12(x1)) → U12Active(mark(x1))
U12Active(x1) → U12(x1)
mark(U21(x1, x2)) → U21Active(mark(x1), x2)
U21Active(x1, x2) → U21(x1, x2)
mark(U22(x1)) → U22Active(mark(x1))
U22Active(x1) → U22(x1)
mark(U31(x1, x2)) → U31Active(mark(x1), x2)
U31Active(x1, x2) → U31(x1, x2)
mark(U32(x1)) → U32Active(mark(x1))
U32Active(x1) → U32(x1)
mark(U41(x1, x2, x3)) → U41Active(mark(x1), x2, x3)
U41Active(x1, x2, x3) → U41(x1, x2, x3)
mark(U42(x1, x2)) → U42Active(mark(x1), x2)
U42Active(x1, x2) → U42(x1, x2)
mark(U43(x1)) → U43Active(mark(x1))
U43Active(x1) → U43(x1)
mark(U51(x1, x2, x3)) → U51Active(mark(x1), x2, x3)
U51Active(x1, x2, x3) → U51(x1, x2, x3)
mark(U52(x1, x2)) → U52Active(mark(x1), x2)
U52Active(x1, x2) → U52(x1, x2)
mark(U53(x1)) → U53Active(mark(x1))
U53Active(x1) → U53(x1)
mark(U61(x1, x2)) → U61Active(mark(x1), x2)
U61Active(x1, x2) → U61(x1, x2)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatIListKind(x1)) → isNatIListKindActive(x1)
isNatIListKindActive(x1) → isNatIListKind(x1)
mark(isNatKind(x1)) → isNatKindActive(x1)
isNatKindActive(x1) → isNatKind(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, V1) → U12Active(isNatListActive(V1))
U12Active(tt) → tt
U21Active(tt, V1) → U22Active(isNatActive(V1))
U22Active(tt) → tt
U31Active(tt, V) → U32Active(isNatListActive(V))
U32Active(tt) → tt
U41Active(tt, V1, V2) → U42Active(isNatActive(V1), V2)
U42Active(tt, V2) → U43Active(isNatIListActive(V2))
U43Active(tt) → tt
U51Active(tt, V1, V2) → U52Active(isNatActive(V1), V2)
U52Active(tt, V2) → U53Active(isNatListActive(V2))
U53Active(tt) → tt
U61Active(tt, L) → s(lengthActive(mark(L)))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → U11Active(isNatIListKindActive(V1), V1)
isNatActive(s(V1)) → U21Active(isNatKindActive(V1), V1)
isNatIListActive(V) → U31Active(isNatIListKindActive(V), V)
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → U41Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
isNatIListKindActive(nil) → tt
isNatIListKindActive(zeros) → tt
isNatIListKindActive(cons(V1, V2)) → andActive(isNatKindActive(V1), isNatIListKind(V2))
isNatKindActive(0) → tt
isNatKindActive(length(V1)) → isNatIListKindActive(V1)
isNatKindActive(s(V1)) → isNatKindActive(V1)
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → U51Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U61Active(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

MARK(U11(x1, x2)) → MARK(x1)
U11ACTIVE(tt, V1) → U12ACTIVE(isNatListActive(V1))
MARK(isNatKind(x1)) → ISNATKINDACTIVE(x1)
MARK(U42(x1, x2)) → U42ACTIVE(mark(x1), x2)
MARK(cons(x1, x2)) → MARK(x1)
U51ACTIVE(tt, V1, V2) → U52ACTIVE(isNatActive(V1), V2)
U51ACTIVE(tt, V1, V2) → ISNATACTIVE(V1)
MARK(U12(x1)) → U12ACTIVE(mark(x1))
MARK(and(x1, x2)) → ANDACTIVE(mark(x1), x2)
MARK(length(x1)) → MARK(x1)
ISNATILISTKINDACTIVE(cons(V1, V2)) → ANDACTIVE(isNatKindActive(V1), isNatIListKind(V2))
MARK(U32(x1)) → U32ACTIVE(mark(x1))
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
ISNATLISTACTIVE(cons(V1, V2)) → ISNATKINDACTIVE(V1)
MARK(U51(x1, x2, x3)) → MARK(x1)
MARK(U53(x1)) → U53ACTIVE(mark(x1))
MARK(U53(x1)) → MARK(x1)
ISNATILISTACTIVE(V) → ISNATILISTKINDACTIVE(V)
ISNATILISTACTIVE(cons(V1, V2)) → U41ACTIVE(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
MARK(U41(x1, x2, x3)) → MARK(x1)
ISNATACTIVE(s(V1)) → U21ACTIVE(isNatKindActive(V1), V1)
MARK(U11(x1, x2)) → U11ACTIVE(mark(x1), x2)
ISNATKINDACTIVE(s(V1)) → ISNATKINDACTIVE(V1)
U61ACTIVE(tt, L) → LENGTHACTIVE(mark(L))
MARK(U43(x1)) → U43ACTIVE(mark(x1))
LENGTHACTIVE(cons(N, L)) → U61ACTIVE(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)
MARK(U32(x1)) → MARK(x1)
MARK(U22(x1)) → MARK(x1)
LENGTHACTIVE(cons(N, L)) → ANDACTIVE(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N)))
ISNATACTIVE(s(V1)) → ISNATKINDACTIVE(V1)
LENGTHACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
MARK(U51(x1, x2, x3)) → U51ACTIVE(mark(x1), x2, x3)
U21ACTIVE(tt, V1) → U22ACTIVE(isNatActive(V1))
U61ACTIVE(tt, L) → MARK(L)
MARK(U21(x1, x2)) → MARK(x1)
U41ACTIVE(tt, V1, V2) → ISNATACTIVE(V1)
MARK(U42(x1, x2)) → MARK(x1)
U41ACTIVE(tt, V1, V2) → U42ACTIVE(isNatActive(V1), V2)
MARK(U52(x1, x2)) → MARK(x1)
MARK(U12(x1)) → MARK(x1)
MARK(length(x1)) → LENGTHACTIVE(mark(x1))
ISNATACTIVE(length(V1)) → ISNATILISTKINDACTIVE(V1)
MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(s(x1)) → MARK(x1)
ISNATLISTACTIVE(cons(V1, V2)) → U51ACTIVE(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
MARK(U31(x1, x2)) → MARK(x1)
U11ACTIVE(tt, V1) → ISNATLISTACTIVE(V1)
ISNATILISTKINDACTIVE(cons(V1, V2)) → ISNATKINDACTIVE(V1)
MARK(zeros) → ZEROSACTIVE
ISNATACTIVE(length(V1)) → U11ACTIVE(isNatIListKindActive(V1), V1)
ANDACTIVE(tt, X) → MARK(X)
MARK(U52(x1, x2)) → U52ACTIVE(mark(x1), x2)
LENGTHACTIVE(cons(N, L)) → ANDACTIVE(isNatListActive(L), isNatIListKind(L))
MARK(and(x1, x2)) → MARK(x1)
MARK(U61(x1, x2)) → U61ACTIVE(mark(x1), x2)
MARK(isNat(x1)) → ISNATACTIVE(x1)
MARK(U41(x1, x2, x3)) → U41ACTIVE(mark(x1), x2, x3)
ISNATKINDACTIVE(length(V1)) → ISNATILISTKINDACTIVE(V1)
MARK(U21(x1, x2)) → U21ACTIVE(mark(x1), x2)
ISNATILISTACTIVE(V) → U31ACTIVE(isNatIListKindActive(V), V)
U42ACTIVE(tt, V2) → U43ACTIVE(isNatIListActive(V2))
MARK(U22(x1)) → U22ACTIVE(mark(x1))
MARK(U61(x1, x2)) → MARK(x1)
MARK(U43(x1)) → MARK(x1)
U21ACTIVE(tt, V1) → ISNATACTIVE(V1)
U31ACTIVE(tt, V) → ISNATLISTACTIVE(V)
ISNATILISTACTIVE(cons(V1, V2)) → ISNATKINDACTIVE(V1)
U31ACTIVE(tt, V) → U32ACTIVE(isNatListActive(V))
ISNATILISTACTIVE(cons(V1, V2)) → ANDACTIVE(isNatKindActive(V1), isNatIListKind(V2))
U52ACTIVE(tt, V2) → U53ACTIVE(isNatListActive(V2))
ISNATLISTACTIVE(cons(V1, V2)) → ANDACTIVE(isNatKindActive(V1), isNatIListKind(V2))
MARK(U31(x1, x2)) → U31ACTIVE(mark(x1), x2)
U42ACTIVE(tt, V2) → ISNATILISTACTIVE(V2)
U52ACTIVE(tt, V2) → ISNATLISTACTIVE(V2)
MARK(isNatIListKind(x1)) → ISNATILISTKINDACTIVE(x1)

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U12(x1)) → U12Active(mark(x1))
U12Active(x1) → U12(x1)
mark(U21(x1, x2)) → U21Active(mark(x1), x2)
U21Active(x1, x2) → U21(x1, x2)
mark(U22(x1)) → U22Active(mark(x1))
U22Active(x1) → U22(x1)
mark(U31(x1, x2)) → U31Active(mark(x1), x2)
U31Active(x1, x2) → U31(x1, x2)
mark(U32(x1)) → U32Active(mark(x1))
U32Active(x1) → U32(x1)
mark(U41(x1, x2, x3)) → U41Active(mark(x1), x2, x3)
U41Active(x1, x2, x3) → U41(x1, x2, x3)
mark(U42(x1, x2)) → U42Active(mark(x1), x2)
U42Active(x1, x2) → U42(x1, x2)
mark(U43(x1)) → U43Active(mark(x1))
U43Active(x1) → U43(x1)
mark(U51(x1, x2, x3)) → U51Active(mark(x1), x2, x3)
U51Active(x1, x2, x3) → U51(x1, x2, x3)
mark(U52(x1, x2)) → U52Active(mark(x1), x2)
U52Active(x1, x2) → U52(x1, x2)
mark(U53(x1)) → U53Active(mark(x1))
U53Active(x1) → U53(x1)
mark(U61(x1, x2)) → U61Active(mark(x1), x2)
U61Active(x1, x2) → U61(x1, x2)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatIListKind(x1)) → isNatIListKindActive(x1)
isNatIListKindActive(x1) → isNatIListKind(x1)
mark(isNatKind(x1)) → isNatKindActive(x1)
isNatKindActive(x1) → isNatKind(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, V1) → U12Active(isNatListActive(V1))
U12Active(tt) → tt
U21Active(tt, V1) → U22Active(isNatActive(V1))
U22Active(tt) → tt
U31Active(tt, V) → U32Active(isNatListActive(V))
U32Active(tt) → tt
U41Active(tt, V1, V2) → U42Active(isNatActive(V1), V2)
U42Active(tt, V2) → U43Active(isNatIListActive(V2))
U43Active(tt) → tt
U51Active(tt, V1, V2) → U52Active(isNatActive(V1), V2)
U52Active(tt, V2) → U53Active(isNatListActive(V2))
U53Active(tt) → tt
U61Active(tt, L) → s(lengthActive(mark(L)))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → U11Active(isNatIListKindActive(V1), V1)
isNatActive(s(V1)) → U21Active(isNatKindActive(V1), V1)
isNatIListActive(V) → U31Active(isNatIListKindActive(V), V)
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → U41Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
isNatIListKindActive(nil) → tt
isNatIListKindActive(zeros) → tt
isNatIListKindActive(cons(V1, V2)) → andActive(isNatKindActive(V1), isNatIListKind(V2))
isNatKindActive(0) → tt
isNatKindActive(length(V1)) → isNatIListKindActive(V1)
isNatKindActive(s(V1)) → isNatKindActive(V1)
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → U51Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U61Active(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 11 less nodes.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

MARK(U11(x1, x2)) → MARK(x1)
MARK(isNatKind(x1)) → ISNATKINDACTIVE(x1)
MARK(U42(x1, x2)) → U42ACTIVE(mark(x1), x2)
MARK(cons(x1, x2)) → MARK(x1)
U51ACTIVE(tt, V1, V2) → U52ACTIVE(isNatActive(V1), V2)
U51ACTIVE(tt, V1, V2) → ISNATACTIVE(V1)
MARK(length(x1)) → MARK(x1)
MARK(and(x1, x2)) → ANDACTIVE(mark(x1), x2)
ISNATILISTKINDACTIVE(cons(V1, V2)) → ANDACTIVE(isNatKindActive(V1), isNatIListKind(V2))
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
ISNATLISTACTIVE(cons(V1, V2)) → ISNATKINDACTIVE(V1)
MARK(U51(x1, x2, x3)) → MARK(x1)
MARK(U53(x1)) → MARK(x1)
ISNATILISTACTIVE(V) → ISNATILISTKINDACTIVE(V)
ISNATILISTACTIVE(cons(V1, V2)) → U41ACTIVE(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
MARK(U41(x1, x2, x3)) → MARK(x1)
ISNATACTIVE(s(V1)) → U21ACTIVE(isNatKindActive(V1), V1)
MARK(U11(x1, x2)) → U11ACTIVE(mark(x1), x2)
ISNATKINDACTIVE(s(V1)) → ISNATKINDACTIVE(V1)
U61ACTIVE(tt, L) → LENGTHACTIVE(mark(L))
MARK(U32(x1)) → MARK(x1)
LENGTHACTIVE(cons(N, L)) → U61ACTIVE(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)
MARK(U22(x1)) → MARK(x1)
LENGTHACTIVE(cons(N, L)) → ANDACTIVE(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N)))
ISNATACTIVE(s(V1)) → ISNATKINDACTIVE(V1)
LENGTHACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
MARK(U51(x1, x2, x3)) → U51ACTIVE(mark(x1), x2, x3)
MARK(U21(x1, x2)) → MARK(x1)
U41ACTIVE(tt, V1, V2) → ISNATACTIVE(V1)
U61ACTIVE(tt, L) → MARK(L)
MARK(U42(x1, x2)) → MARK(x1)
U41ACTIVE(tt, V1, V2) → U42ACTIVE(isNatActive(V1), V2)
MARK(length(x1)) → LENGTHACTIVE(mark(x1))
MARK(U12(x1)) → MARK(x1)
MARK(U52(x1, x2)) → MARK(x1)
ISNATACTIVE(length(V1)) → ISNATILISTKINDACTIVE(V1)
MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(s(x1)) → MARK(x1)
ISNATLISTACTIVE(cons(V1, V2)) → U51ACTIVE(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
MARK(U31(x1, x2)) → MARK(x1)
U11ACTIVE(tt, V1) → ISNATLISTACTIVE(V1)
ISNATILISTKINDACTIVE(cons(V1, V2)) → ISNATKINDACTIVE(V1)
ANDACTIVE(tt, X) → MARK(X)
ISNATACTIVE(length(V1)) → U11ACTIVE(isNatIListKindActive(V1), V1)
MARK(U52(x1, x2)) → U52ACTIVE(mark(x1), x2)
LENGTHACTIVE(cons(N, L)) → ANDACTIVE(isNatListActive(L), isNatIListKind(L))
MARK(and(x1, x2)) → MARK(x1)
MARK(isNat(x1)) → ISNATACTIVE(x1)
MARK(U61(x1, x2)) → U61ACTIVE(mark(x1), x2)
MARK(U41(x1, x2, x3)) → U41ACTIVE(mark(x1), x2, x3)
ISNATKINDACTIVE(length(V1)) → ISNATILISTKINDACTIVE(V1)
MARK(U21(x1, x2)) → U21ACTIVE(mark(x1), x2)
ISNATILISTACTIVE(V) → U31ACTIVE(isNatIListKindActive(V), V)
MARK(U61(x1, x2)) → MARK(x1)
MARK(U43(x1)) → MARK(x1)
U21ACTIVE(tt, V1) → ISNATACTIVE(V1)
U31ACTIVE(tt, V) → ISNATLISTACTIVE(V)
ISNATILISTACTIVE(cons(V1, V2)) → ISNATKINDACTIVE(V1)
ISNATILISTACTIVE(cons(V1, V2)) → ANDACTIVE(isNatKindActive(V1), isNatIListKind(V2))
ISNATLISTACTIVE(cons(V1, V2)) → ANDACTIVE(isNatKindActive(V1), isNatIListKind(V2))
MARK(U31(x1, x2)) → U31ACTIVE(mark(x1), x2)
U42ACTIVE(tt, V2) → ISNATILISTACTIVE(V2)
U52ACTIVE(tt, V2) → ISNATLISTACTIVE(V2)
MARK(isNatIListKind(x1)) → ISNATILISTKINDACTIVE(x1)

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U12(x1)) → U12Active(mark(x1))
U12Active(x1) → U12(x1)
mark(U21(x1, x2)) → U21Active(mark(x1), x2)
U21Active(x1, x2) → U21(x1, x2)
mark(U22(x1)) → U22Active(mark(x1))
U22Active(x1) → U22(x1)
mark(U31(x1, x2)) → U31Active(mark(x1), x2)
U31Active(x1, x2) → U31(x1, x2)
mark(U32(x1)) → U32Active(mark(x1))
U32Active(x1) → U32(x1)
mark(U41(x1, x2, x3)) → U41Active(mark(x1), x2, x3)
U41Active(x1, x2, x3) → U41(x1, x2, x3)
mark(U42(x1, x2)) → U42Active(mark(x1), x2)
U42Active(x1, x2) → U42(x1, x2)
mark(U43(x1)) → U43Active(mark(x1))
U43Active(x1) → U43(x1)
mark(U51(x1, x2, x3)) → U51Active(mark(x1), x2, x3)
U51Active(x1, x2, x3) → U51(x1, x2, x3)
mark(U52(x1, x2)) → U52Active(mark(x1), x2)
U52Active(x1, x2) → U52(x1, x2)
mark(U53(x1)) → U53Active(mark(x1))
U53Active(x1) → U53(x1)
mark(U61(x1, x2)) → U61Active(mark(x1), x2)
U61Active(x1, x2) → U61(x1, x2)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatIListKind(x1)) → isNatIListKindActive(x1)
isNatIListKindActive(x1) → isNatIListKind(x1)
mark(isNatKind(x1)) → isNatKindActive(x1)
isNatKindActive(x1) → isNatKind(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, V1) → U12Active(isNatListActive(V1))
U12Active(tt) → tt
U21Active(tt, V1) → U22Active(isNatActive(V1))
U22Active(tt) → tt
U31Active(tt, V) → U32Active(isNatListActive(V))
U32Active(tt) → tt
U41Active(tt, V1, V2) → U42Active(isNatActive(V1), V2)
U42Active(tt, V2) → U43Active(isNatIListActive(V2))
U43Active(tt) → tt
U51Active(tt, V1, V2) → U52Active(isNatActive(V1), V2)
U52Active(tt, V2) → U53Active(isNatListActive(V2))
U53Active(tt) → tt
U61Active(tt, L) → s(lengthActive(mark(L)))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → U11Active(isNatIListKindActive(V1), V1)
isNatActive(s(V1)) → U21Active(isNatKindActive(V1), V1)
isNatIListActive(V) → U31Active(isNatIListKindActive(V), V)
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → U41Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
isNatIListKindActive(nil) → tt
isNatIListKindActive(zeros) → tt
isNatIListKindActive(cons(V1, V2)) → andActive(isNatKindActive(V1), isNatIListKind(V2))
isNatKindActive(0) → tt
isNatKindActive(length(V1)) → isNatIListKindActive(V1)
isNatKindActive(s(V1)) → isNatKindActive(V1)
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → U51Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U61Active(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

MARK(length(x1)) → MARK(x1)
MARK(length(x1)) → LENGTHACTIVE(mark(x1))
MARK(U61(x1, x2)) → U61ACTIVE(mark(x1), x2)
MARK(U61(x1, x2)) → MARK(x1)

The remaining pairs can at least be oriented weakly.

MARK(U11(x1, x2)) → MARK(x1)
MARK(isNatKind(x1)) → ISNATKINDACTIVE(x1)
MARK(U42(x1, x2)) → U42ACTIVE(mark(x1), x2)
MARK(cons(x1, x2)) → MARK(x1)
U51ACTIVE(tt, V1, V2) → U52ACTIVE(isNatActive(V1), V2)
U51ACTIVE(tt, V1, V2) → ISNATACTIVE(V1)
MARK(and(x1, x2)) → ANDACTIVE(mark(x1), x2)
ISNATILISTKINDACTIVE(cons(V1, V2)) → ANDACTIVE(isNatKindActive(V1), isNatIListKind(V2))
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
ISNATLISTACTIVE(cons(V1, V2)) → ISNATKINDACTIVE(V1)
MARK(U51(x1, x2, x3)) → MARK(x1)
MARK(U53(x1)) → MARK(x1)
ISNATILISTACTIVE(V) → ISNATILISTKINDACTIVE(V)
ISNATILISTACTIVE(cons(V1, V2)) → U41ACTIVE(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
MARK(U41(x1, x2, x3)) → MARK(x1)
ISNATACTIVE(s(V1)) → U21ACTIVE(isNatKindActive(V1), V1)
MARK(U11(x1, x2)) → U11ACTIVE(mark(x1), x2)
ISNATKINDACTIVE(s(V1)) → ISNATKINDACTIVE(V1)
U61ACTIVE(tt, L) → LENGTHACTIVE(mark(L))
MARK(U32(x1)) → MARK(x1)
LENGTHACTIVE(cons(N, L)) → U61ACTIVE(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)
MARK(U22(x1)) → MARK(x1)
LENGTHACTIVE(cons(N, L)) → ANDACTIVE(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N)))
ISNATACTIVE(s(V1)) → ISNATKINDACTIVE(V1)
LENGTHACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
MARK(U51(x1, x2, x3)) → U51ACTIVE(mark(x1), x2, x3)
MARK(U21(x1, x2)) → MARK(x1)
U41ACTIVE(tt, V1, V2) → ISNATACTIVE(V1)
U61ACTIVE(tt, L) → MARK(L)
MARK(U42(x1, x2)) → MARK(x1)
U41ACTIVE(tt, V1, V2) → U42ACTIVE(isNatActive(V1), V2)
MARK(U12(x1)) → MARK(x1)
MARK(U52(x1, x2)) → MARK(x1)
ISNATACTIVE(length(V1)) → ISNATILISTKINDACTIVE(V1)
MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(s(x1)) → MARK(x1)
ISNATLISTACTIVE(cons(V1, V2)) → U51ACTIVE(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
MARK(U31(x1, x2)) → MARK(x1)
U11ACTIVE(tt, V1) → ISNATLISTACTIVE(V1)
ISNATILISTKINDACTIVE(cons(V1, V2)) → ISNATKINDACTIVE(V1)
ANDACTIVE(tt, X) → MARK(X)
ISNATACTIVE(length(V1)) → U11ACTIVE(isNatIListKindActive(V1), V1)
MARK(U52(x1, x2)) → U52ACTIVE(mark(x1), x2)
LENGTHACTIVE(cons(N, L)) → ANDACTIVE(isNatListActive(L), isNatIListKind(L))
MARK(and(x1, x2)) → MARK(x1)
MARK(isNat(x1)) → ISNATACTIVE(x1)
MARK(U41(x1, x2, x3)) → U41ACTIVE(mark(x1), x2, x3)
ISNATKINDACTIVE(length(V1)) → ISNATILISTKINDACTIVE(V1)
MARK(U21(x1, x2)) → U21ACTIVE(mark(x1), x2)
ISNATILISTACTIVE(V) → U31ACTIVE(isNatIListKindActive(V), V)
MARK(U43(x1)) → MARK(x1)
U21ACTIVE(tt, V1) → ISNATACTIVE(V1)
U31ACTIVE(tt, V) → ISNATLISTACTIVE(V)
ISNATILISTACTIVE(cons(V1, V2)) → ISNATKINDACTIVE(V1)
ISNATILISTACTIVE(cons(V1, V2)) → ANDACTIVE(isNatKindActive(V1), isNatIListKind(V2))
ISNATLISTACTIVE(cons(V1, V2)) → ANDACTIVE(isNatKindActive(V1), isNatIListKind(V2))
MARK(U31(x1, x2)) → U31ACTIVE(mark(x1), x2)
U42ACTIVE(tt, V2) → ISNATILISTACTIVE(V2)
U52ACTIVE(tt, V2) → ISNATLISTACTIVE(V2)
MARK(isNatIListKind(x1)) → ISNATILISTKINDACTIVE(x1)

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(ANDACTIVE(x₁, x₂)) = x₂
POL(ISNATACTIVE(x₁)) = 0
POL(ISNATILISTACTIVE(x₁)) = x₁
POL(ISNATILISTKINDACTIVE(x₁)) = 0
POL(ISNATKINDACTIVE(x₁)) = 0
POL(ISNATLISTACTIVE(x₁)) = 0
POL(LENGTHACTIVE(x₁)) = x₁
POL(MARK(x₁)) = x₁
POL(U11(x₁, x₂)) = x₁
POL(U11ACTIVE(x₁, x₂)) = 0
POL(U11Active(x₁, x₂)) = x₁
POL(U12(x₁)) = x₁
POL(U12Active(x₁)) = x₁
POL(U21(x₁, x₂)) = x₁
POL(U21ACTIVE(x₁, x₂)) = 0
POL(U21Active(x₁, x₂)) = x₁
POL(U22(x₁)) = x₁
POL(U22Active(x₁)) = x₁
POL(U31(x₁, x₂)) = x₁
POL(U31ACTIVE(x₁, x₂)) = 0
POL(U31Active(x₁, x₂)) = x₁
POL(U32(x₁)) = x₁
POL(U32Active(x₁)) = x₁
POL(U41(x₁, x₂, x₃)) = x₁ + x₃
POL(U41ACTIVE(x₁, x₂, x₃)) = x₃
POL(U41Active(x₁, x₂, x₃)) = x₁ + x₃
POL(U42(x₁, x₂)) = x₁ + x₂
POL(U42ACTIVE(x₁, x₂)) = x₂
POL(U42Active(x₁, x₂)) = x₁ + x₂
POL(U43(x₁)) = x₁
POL(U43Active(x₁)) = x₁
POL(U51(x₁, x₂, x₃)) = x₁
POL(U51ACTIVE(x₁, x₂, x₃)) = 0
POL(U51Active(x₁, x₂, x₃)) = x₁
POL(U52(x₁, x₂)) = x₁
POL(U52ACTIVE(x₁, x₂)) = 0
POL(U52Active(x₁, x₂)) = x₁
POL(U53(x₁)) = x₁
POL(U53Active(x₁)) = x₁
POL(U61(x₁, x₂)) = 1 + x₁ + x₂
POL(U61ACTIVE(x₁, x₂)) = x₂
POL(U61Active(x₁, x₂)) = 1 + x₁ + x₂
POL(and(x₁, x₂)) = x₁ + x₂
POL(andActive(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = x₁ + x₂
POL(isNat(x₁)) = 0
POL(isNatActive(x₁)) = 0
POL(isNatIList(x₁)) = x₁
POL(isNatIListActive(x₁)) = x₁
POL(isNatIListKind(x₁)) = 0
POL(isNatIListKindActive(x₁)) = 0
POL(isNatKind(x₁)) = 0
POL(isNatKindActive(x₁)) = 0
POL(isNatList(x₁)) = 0
POL(isNatListActive(x₁)) = 0
POL(length(x₁)) = 1 + x₁
POL(lengthActive(x₁)) = 1 + x₁
POL(mark(x₁)) = x₁
POL(nil) = 0
POL(s(x₁)) = x₁
POL(tt) = 0
POL(zeros) = 0
POL(zerosActive) = 0

The following usable rules [17] were oriented:

isNatKindActive(0) → tt
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → U41Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
isNatIListKindActive(nil) → tt
mark(zeros) → zerosActive
zerosActive → zeros
isNatIListKindActive(zeros) → tt
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → U51Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U61Active(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
isNatKindActive(length(V1)) → isNatIListKindActive(V1)
isNatIListKindActive(cons(V1, V2)) → andActive(isNatKindActive(V1), isNatIListKind(V2))
mark(isNatKind(x1)) → isNatKindActive(x1)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(tt, X) → mark(X)
mark(isNatIListKind(x1)) → isNatIListKindActive(x1)
isNatKindActive(s(V1)) → isNatKindActive(V1)
andActive(x1, x2) → and(x1, x2)
mark(U61(x1, x2)) → U61Active(mark(x1), x2)
U61Active(x1, x2) → U61(x1, x2)
mark(U53(x1)) → U53Active(mark(x1))
U53Active(x1) → U53(x1)
mark(U52(x1, x2)) → U52Active(mark(x1), x2)
U52Active(x1, x2) → U52(x1, x2)
mark(U51(x1, x2, x3)) → U51Active(mark(x1), x2, x3)
U51Active(x1, x2, x3) → U51(x1, x2, x3)
mark(U43(x1)) → U43Active(mark(x1))
U43Active(x1) → U43(x1)
U42Active(x1, x2) → U42(x1, x2)
mark(U42(x1, x2)) → U42Active(mark(x1), x2)
U41Active(x1, x2, x3) → U41(x1, x2, x3)
mark(U41(x1, x2, x3)) → U41Active(mark(x1), x2, x3)
U32Active(x1) → U32(x1)
mark(U32(x1)) → U32Active(mark(x1))
U31Active(x1, x2) → U31(x1, x2)
mark(U31(x1, x2)) → U31Active(mark(x1), x2)
U22Active(x1) → U22(x1)
mark(U22(x1)) → U22Active(mark(x1))
U21Active(x1, x2) → U21(x1, x2)
mark(U21(x1, x2)) → U21Active(mark(x1), x2)
U12Active(x1) → U12(x1)
mark(U12(x1)) → U12Active(mark(x1))
U11Active(x1, x2) → U11(x1, x2)
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
isNatActive(0) → tt
isNatActive(length(V1)) → U11Active(isNatIListKindActive(V1), V1)
isNatActive(s(V1)) → U21Active(isNatKindActive(V1), V1)
isNatIListActive(V) → U31Active(isNatIListKindActive(V), V)
U52Active(tt, V2) → U53Active(isNatListActive(V2))
U53Active(tt) → tt
U61Active(tt, L) → s(lengthActive(mark(L)))
U41Active(tt, V1, V2) → U42Active(isNatActive(V1), V2)
U42Active(tt, V2) → U43Active(isNatIListActive(V2))
U43Active(tt) → tt
U51Active(tt, V1, V2) → U52Active(isNatActive(V1), V2)
U21Active(tt, V1) → U22Active(isNatActive(V1))
U22Active(tt) → tt
U31Active(tt, V) → U32Active(isNatListActive(V))
U32Active(tt) → tt
zerosActive → cons(0, zeros)
mark(nil) → nil
U12Active(tt) → tt
U11Active(tt, V1) → U12Active(isNatListActive(V1))
mark(0) → 0
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(s(x1)) → s(mark(x1))
mark(tt) → tt
isNatListActive(x1) → isNatList(x1)
mark(isNatList(x1)) → isNatListActive(x1)
lengthActive(x1) → length(x1)
mark(length(x1)) → lengthActive(mark(x1))
isNatIListKindActive(x1) → isNatIListKind(x1)
isNatKindActive(x1) → isNatKind(x1)

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

MARK(U11(x1, x2)) → MARK(x1)
MARK(isNatKind(x1)) → ISNATKINDACTIVE(x1)
MARK(U42(x1, x2)) → U42ACTIVE(mark(x1), x2)
MARK(cons(x1, x2)) → MARK(x1)
U51ACTIVE(tt, V1, V2) → U52ACTIVE(isNatActive(V1), V2)
U51ACTIVE(tt, V1, V2) → ISNATACTIVE(V1)
MARK(and(x1, x2)) → ANDACTIVE(mark(x1), x2)
ISNATILISTKINDACTIVE(cons(V1, V2)) → ANDACTIVE(isNatKindActive(V1), isNatIListKind(V2))
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
ISNATLISTACTIVE(cons(V1, V2)) → ISNATKINDACTIVE(V1)
MARK(U51(x1, x2, x3)) → MARK(x1)
MARK(U53(x1)) → MARK(x1)
ISNATILISTACTIVE(V) → ISNATILISTKINDACTIVE(V)
ISNATILISTACTIVE(cons(V1, V2)) → U41ACTIVE(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
MARK(U41(x1, x2, x3)) → MARK(x1)
MARK(U11(x1, x2)) → U11ACTIVE(mark(x1), x2)
ISNATACTIVE(s(V1)) → U21ACTIVE(isNatKindActive(V1), V1)
ISNATKINDACTIVE(s(V1)) → ISNATKINDACTIVE(V1)
U61ACTIVE(tt, L) → LENGTHACTIVE(mark(L))
LENGTHACTIVE(cons(N, L)) → U61ACTIVE(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)
MARK(U32(x1)) → MARK(x1)
MARK(U22(x1)) → MARK(x1)
LENGTHACTIVE(cons(N, L)) → ANDACTIVE(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N)))
ISNATACTIVE(s(V1)) → ISNATKINDACTIVE(V1)
LENGTHACTIVE(cons(N, L)) → ISNATLISTACTIVE(L)
MARK(U51(x1, x2, x3)) → U51ACTIVE(mark(x1), x2, x3)
MARK(U21(x1, x2)) → MARK(x1)
U41ACTIVE(tt, V1, V2) → ISNATACTIVE(V1)
U61ACTIVE(tt, L) → MARK(L)
MARK(U42(x1, x2)) → MARK(x1)
U41ACTIVE(tt, V1, V2) → U42ACTIVE(isNatActive(V1), V2)
MARK(U12(x1)) → MARK(x1)
MARK(U52(x1, x2)) → MARK(x1)
ISNATACTIVE(length(V1)) → ISNATILISTKINDACTIVE(V1)
MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(s(x1)) → MARK(x1)
ISNATLISTACTIVE(cons(V1, V2)) → U51ACTIVE(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
MARK(U31(x1, x2)) → MARK(x1)
U11ACTIVE(tt, V1) → ISNATLISTACTIVE(V1)
ISNATILISTKINDACTIVE(cons(V1, V2)) → ISNATKINDACTIVE(V1)
ANDACTIVE(tt, X) → MARK(X)
ISNATACTIVE(length(V1)) → U11ACTIVE(isNatIListKindActive(V1), V1)
MARK(U52(x1, x2)) → U52ACTIVE(mark(x1), x2)
LENGTHACTIVE(cons(N, L)) → ANDACTIVE(isNatListActive(L), isNatIListKind(L))
MARK(and(x1, x2)) → MARK(x1)
MARK(isNat(x1)) → ISNATACTIVE(x1)
MARK(U41(x1, x2, x3)) → U41ACTIVE(mark(x1), x2, x3)
ISNATKINDACTIVE(length(V1)) → ISNATILISTKINDACTIVE(V1)
MARK(U21(x1, x2)) → U21ACTIVE(mark(x1), x2)
ISNATILISTACTIVE(V) → U31ACTIVE(isNatIListKindActive(V), V)
MARK(U43(x1)) → MARK(x1)
U21ACTIVE(tt, V1) → ISNATACTIVE(V1)
U31ACTIVE(tt, V) → ISNATLISTACTIVE(V)
ISNATILISTACTIVE(cons(V1, V2)) → ISNATKINDACTIVE(V1)
ISNATILISTACTIVE(cons(V1, V2)) → ANDACTIVE(isNatKindActive(V1), isNatIListKind(V2))
ISNATLISTACTIVE(cons(V1, V2)) → ANDACTIVE(isNatKindActive(V1), isNatIListKind(V2))
U42ACTIVE(tt, V2) → ISNATILISTACTIVE(V2)
MARK(U31(x1, x2)) → U31ACTIVE(mark(x1), x2)
U52ACTIVE(tt, V2) → ISNATLISTACTIVE(V2)
MARK(isNatIListKind(x1)) → ISNATILISTKINDACTIVE(x1)

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U12(x1)) → U12Active(mark(x1))
U12Active(x1) → U12(x1)
mark(U21(x1, x2)) → U21Active(mark(x1), x2)
U21Active(x1, x2) → U21(x1, x2)
mark(U22(x1)) → U22Active(mark(x1))
U22Active(x1) → U22(x1)
mark(U31(x1, x2)) → U31Active(mark(x1), x2)
U31Active(x1, x2) → U31(x1, x2)
mark(U32(x1)) → U32Active(mark(x1))
U32Active(x1) → U32(x1)
mark(U41(x1, x2, x3)) → U41Active(mark(x1), x2, x3)
U41Active(x1, x2, x3) → U41(x1, x2, x3)
mark(U42(x1, x2)) → U42Active(mark(x1), x2)
U42Active(x1, x2) → U42(x1, x2)
mark(U43(x1)) → U43Active(mark(x1))
U43Active(x1) → U43(x1)
mark(U51(x1, x2, x3)) → U51Active(mark(x1), x2, x3)
U51Active(x1, x2, x3) → U51(x1, x2, x3)
mark(U52(x1, x2)) → U52Active(mark(x1), x2)
U52Active(x1, x2) → U52(x1, x2)
mark(U53(x1)) → U53Active(mark(x1))
U53Active(x1) → U53(x1)
mark(U61(x1, x2)) → U61Active(mark(x1), x2)
U61Active(x1, x2) → U61(x1, x2)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatIListKind(x1)) → isNatIListKindActive(x1)
isNatIListKindActive(x1) → isNatIListKind(x1)
mark(isNatKind(x1)) → isNatKindActive(x1)
isNatKindActive(x1) → isNatKind(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, V1) → U12Active(isNatListActive(V1))
U12Active(tt) → tt
U21Active(tt, V1) → U22Active(isNatActive(V1))
U22Active(tt) → tt
U31Active(tt, V) → U32Active(isNatListActive(V))
U32Active(tt) → tt
U41Active(tt, V1, V2) → U42Active(isNatActive(V1), V2)
U42Active(tt, V2) → U43Active(isNatIListActive(V2))
U43Active(tt) → tt
U51Active(tt, V1, V2) → U52Active(isNatActive(V1), V2)
U52Active(tt, V2) → U53Active(isNatListActive(V2))
U53Active(tt) → tt
U61Active(tt, L) → s(lengthActive(mark(L)))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → U11Active(isNatIListKindActive(V1), V1)
isNatActive(s(V1)) → U21Active(isNatKindActive(V1), V1)
isNatIListActive(V) → U31Active(isNatIListKindActive(V), V)
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → U41Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
isNatIListKindActive(nil) → tt
isNatIListKindActive(zeros) → tt
isNatIListKindActive(cons(V1, V2)) → andActive(isNatKindActive(V1), isNatIListKind(V2))
isNatKindActive(0) → tt
isNatKindActive(length(V1)) → isNatIListKindActive(V1)
isNatKindActive(s(V1)) → isNatKindActive(V1)
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → U51Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U61Active(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 4 less nodes.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                        ↳ QDPOrderProof

                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

MARK(U11(x1, x2)) → MARK(x1)
MARK(isNatKind(x1)) → ISNATKINDACTIVE(x1)
MARK(U42(x1, x2)) → U42ACTIVE(mark(x1), x2)
MARK(cons(x1, x2)) → MARK(x1)
U51ACTIVE(tt, V1, V2) → U52ACTIVE(isNatActive(V1), V2)
U51ACTIVE(tt, V1, V2) → ISNATACTIVE(V1)
MARK(and(x1, x2)) → ANDACTIVE(mark(x1), x2)
ISNATILISTKINDACTIVE(cons(V1, V2)) → ANDACTIVE(isNatKindActive(V1), isNatIListKind(V2))
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
ISNATLISTACTIVE(cons(V1, V2)) → ISNATKINDACTIVE(V1)
MARK(U51(x1, x2, x3)) → MARK(x1)
MARK(U53(x1)) → MARK(x1)
ISNATILISTACTIVE(V) → ISNATILISTKINDACTIVE(V)
ISNATILISTACTIVE(cons(V1, V2)) → U41ACTIVE(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
MARK(U41(x1, x2, x3)) → MARK(x1)
ISNATACTIVE(s(V1)) → U21ACTIVE(isNatKindActive(V1), V1)
MARK(U11(x1, x2)) → U11ACTIVE(mark(x1), x2)
ISNATKINDACTIVE(s(V1)) → ISNATKINDACTIVE(V1)
MARK(U32(x1)) → MARK(x1)
MARK(U22(x1)) → MARK(x1)
ISNATACTIVE(s(V1)) → ISNATKINDACTIVE(V1)
MARK(U51(x1, x2, x3)) → U51ACTIVE(mark(x1), x2, x3)
MARK(U21(x1, x2)) → MARK(x1)
U41ACTIVE(tt, V1, V2) → ISNATACTIVE(V1)
MARK(U42(x1, x2)) → MARK(x1)
U41ACTIVE(tt, V1, V2) → U42ACTIVE(isNatActive(V1), V2)
MARK(U12(x1)) → MARK(x1)
MARK(U52(x1, x2)) → MARK(x1)
ISNATACTIVE(length(V1)) → ISNATILISTKINDACTIVE(V1)
MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(s(x1)) → MARK(x1)
ISNATLISTACTIVE(cons(V1, V2)) → U51ACTIVE(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
MARK(U31(x1, x2)) → MARK(x1)
U11ACTIVE(tt, V1) → ISNATLISTACTIVE(V1)
ISNATILISTKINDACTIVE(cons(V1, V2)) → ISNATKINDACTIVE(V1)
ANDACTIVE(tt, X) → MARK(X)
ISNATACTIVE(length(V1)) → U11ACTIVE(isNatIListKindActive(V1), V1)
MARK(U52(x1, x2)) → U52ACTIVE(mark(x1), x2)
MARK(and(x1, x2)) → MARK(x1)
MARK(isNat(x1)) → ISNATACTIVE(x1)
MARK(U41(x1, x2, x3)) → U41ACTIVE(mark(x1), x2, x3)
ISNATKINDACTIVE(length(V1)) → ISNATILISTKINDACTIVE(V1)
MARK(U21(x1, x2)) → U21ACTIVE(mark(x1), x2)
ISNATILISTACTIVE(V) → U31ACTIVE(isNatIListKindActive(V), V)
MARK(U43(x1)) → MARK(x1)
U21ACTIVE(tt, V1) → ISNATACTIVE(V1)
U31ACTIVE(tt, V) → ISNATLISTACTIVE(V)
ISNATILISTACTIVE(cons(V1, V2)) → ISNATKINDACTIVE(V1)
ISNATILISTACTIVE(cons(V1, V2)) → ANDACTIVE(isNatKindActive(V1), isNatIListKind(V2))
ISNATLISTACTIVE(cons(V1, V2)) → ANDACTIVE(isNatKindActive(V1), isNatIListKind(V2))
MARK(U31(x1, x2)) → U31ACTIVE(mark(x1), x2)
U42ACTIVE(tt, V2) → ISNATILISTACTIVE(V2)
U52ACTIVE(tt, V2) → ISNATLISTACTIVE(V2)
MARK(isNatIListKind(x1)) → ISNATILISTKINDACTIVE(x1)

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U12(x1)) → U12Active(mark(x1))
U12Active(x1) → U12(x1)
mark(U21(x1, x2)) → U21Active(mark(x1), x2)
U21Active(x1, x2) → U21(x1, x2)
mark(U22(x1)) → U22Active(mark(x1))
U22Active(x1) → U22(x1)
mark(U31(x1, x2)) → U31Active(mark(x1), x2)
U31Active(x1, x2) → U31(x1, x2)
mark(U32(x1)) → U32Active(mark(x1))
U32Active(x1) → U32(x1)
mark(U41(x1, x2, x3)) → U41Active(mark(x1), x2, x3)
U41Active(x1, x2, x3) → U41(x1, x2, x3)
mark(U42(x1, x2)) → U42Active(mark(x1), x2)
U42Active(x1, x2) → U42(x1, x2)
mark(U43(x1)) → U43Active(mark(x1))
U43Active(x1) → U43(x1)
mark(U51(x1, x2, x3)) → U51Active(mark(x1), x2, x3)
U51Active(x1, x2, x3) → U51(x1, x2, x3)
mark(U52(x1, x2)) → U52Active(mark(x1), x2)
U52Active(x1, x2) → U52(x1, x2)
mark(U53(x1)) → U53Active(mark(x1))
U53Active(x1) → U53(x1)
mark(U61(x1, x2)) → U61Active(mark(x1), x2)
U61Active(x1, x2) → U61(x1, x2)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatIListKind(x1)) → isNatIListKindActive(x1)
isNatIListKindActive(x1) → isNatIListKind(x1)
mark(isNatKind(x1)) → isNatKindActive(x1)
isNatKindActive(x1) → isNatKind(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, V1) → U12Active(isNatListActive(V1))
U12Active(tt) → tt
U21Active(tt, V1) → U22Active(isNatActive(V1))
U22Active(tt) → tt
U31Active(tt, V) → U32Active(isNatListActive(V))
U32Active(tt) → tt
U41Active(tt, V1, V2) → U42Active(isNatActive(V1), V2)
U42Active(tt, V2) → U43Active(isNatIListActive(V2))
U43Active(tt) → tt
U51Active(tt, V1, V2) → U52Active(isNatActive(V1), V2)
U52Active(tt, V2) → U53Active(isNatListActive(V2))
U53Active(tt) → tt
U61Active(tt, L) → s(lengthActive(mark(L)))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → U11Active(isNatIListKindActive(V1), V1)
isNatActive(s(V1)) → U21Active(isNatKindActive(V1), V1)
isNatIListActive(V) → U31Active(isNatIListKindActive(V), V)
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → U41Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
isNatIListKindActive(nil) → tt
isNatIListKindActive(zeros) → tt
isNatIListKindActive(cons(V1, V2)) → andActive(isNatKindActive(V1), isNatIListKind(V2))
isNatKindActive(0) → tt
isNatKindActive(length(V1)) → isNatIListKindActive(V1)
isNatKindActive(s(V1)) → isNatKindActive(V1)
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → U51Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U61Active(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

MARK(U11(x1, x2)) → MARK(x1)
MARK(isNatKind(x1)) → ISNATKINDACTIVE(x1)
MARK(U42(x1, x2)) → U42ACTIVE(mark(x1), x2)
MARK(cons(x1, x2)) → MARK(x1)
U51ACTIVE(tt, V1, V2) → ISNATACTIVE(V1)
MARK(and(x1, x2)) → ANDACTIVE(mark(x1), x2)
MARK(isNatList(x1)) → ISNATLISTACTIVE(x1)
ISNATLISTACTIVE(cons(V1, V2)) → ISNATKINDACTIVE(V1)
MARK(U51(x1, x2, x3)) → MARK(x1)
MARK(U53(x1)) → MARK(x1)
ISNATILISTACTIVE(cons(V1, V2)) → U41ACTIVE(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
MARK(U41(x1, x2, x3)) → MARK(x1)
MARK(U11(x1, x2)) → U11ACTIVE(mark(x1), x2)
ISNATKINDACTIVE(s(V1)) → ISNATKINDACTIVE(V1)
MARK(U32(x1)) → MARK(x1)
MARK(U22(x1)) → MARK(x1)
MARK(U51(x1, x2, x3)) → U51ACTIVE(mark(x1), x2, x3)
MARK(U21(x1, x2)) → MARK(x1)
U41ACTIVE(tt, V1, V2) → ISNATACTIVE(V1)
MARK(U42(x1, x2)) → MARK(x1)
MARK(U12(x1)) → MARK(x1)
MARK(U52(x1, x2)) → MARK(x1)
MARK(isNatIList(x1)) → ISNATILISTACTIVE(x1)
MARK(s(x1)) → MARK(x1)
ISNATLISTACTIVE(cons(V1, V2)) → U51ACTIVE(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
MARK(U31(x1, x2)) → MARK(x1)
ISNATILISTKINDACTIVE(cons(V1, V2)) → ISNATKINDACTIVE(V1)
MARK(U52(x1, x2)) → U52ACTIVE(mark(x1), x2)
MARK(and(x1, x2)) → MARK(x1)
MARK(isNat(x1)) → ISNATACTIVE(x1)
MARK(U41(x1, x2, x3)) → U41ACTIVE(mark(x1), x2, x3)
ISNATKINDACTIVE(length(V1)) → ISNATILISTKINDACTIVE(V1)
MARK(U21(x1, x2)) → U21ACTIVE(mark(x1), x2)
MARK(U43(x1)) → MARK(x1)
U21ACTIVE(tt, V1) → ISNATACTIVE(V1)
ISNATILISTACTIVE(cons(V1, V2)) → ISNATKINDACTIVE(V1)
MARK(U31(x1, x2)) → U31ACTIVE(mark(x1), x2)
MARK(isNatIListKind(x1)) → ISNATILISTKINDACTIVE(x1)

The remaining pairs can at least be oriented weakly.

U51ACTIVE(tt, V1, V2) → U52ACTIVE(isNatActive(V1), V2)
ISNATILISTKINDACTIVE(cons(V1, V2)) → ANDACTIVE(isNatKindActive(V1), isNatIListKind(V2))
ISNATILISTACTIVE(V) → ISNATILISTKINDACTIVE(V)
ISNATACTIVE(s(V1)) → U21ACTIVE(isNatKindActive(V1), V1)
ISNATACTIVE(s(V1)) → ISNATKINDACTIVE(V1)
U41ACTIVE(tt, V1, V2) → U42ACTIVE(isNatActive(V1), V2)
ISNATACTIVE(length(V1)) → ISNATILISTKINDACTIVE(V1)
U11ACTIVE(tt, V1) → ISNATLISTACTIVE(V1)
ANDACTIVE(tt, X) → MARK(X)
ISNATACTIVE(length(V1)) → U11ACTIVE(isNatIListKindActive(V1), V1)
ISNATILISTACTIVE(V) → U31ACTIVE(isNatIListKindActive(V), V)
U31ACTIVE(tt, V) → ISNATLISTACTIVE(V)
ISNATILISTACTIVE(cons(V1, V2)) → ANDACTIVE(isNatKindActive(V1), isNatIListKind(V2))
ISNATLISTACTIVE(cons(V1, V2)) → ANDACTIVE(isNatKindActive(V1), isNatIListKind(V2))
U42ACTIVE(tt, V2) → ISNATILISTACTIVE(V2)
U52ACTIVE(tt, V2) → ISNATLISTACTIVE(V2)

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(ANDACTIVE(x₁, x₂)) = 1 + x₂
POL(ISNATACTIVE(x₁)) = x₁
POL(ISNATILISTACTIVE(x₁)) = 1 + x₁
POL(ISNATILISTKINDACTIVE(x₁)) = 1 + x₁
POL(ISNATKINDACTIVE(x₁)) = 1 + x₁
POL(ISNATLISTACTIVE(x₁)) = 1 + x₁
POL(MARK(x₁)) = 1 + x₁
POL(U11(x₁, x₂)) = 1 + x₁ + x₂
POL(U11ACTIVE(x₁, x₂)) = 1 + x₂
POL(U11Active(x₁, x₂)) = 0
POL(U12(x₁)) = 1 + x₁
POL(U12Active(x₁)) = 0
POL(U21(x₁, x₂)) = 1 + x₁ + x₂
POL(U21ACTIVE(x₁, x₂)) = 1 + x₂
POL(U21Active(x₁, x₂)) = 0
POL(U22(x₁)) = 1 + x₁
POL(U22Active(x₁)) = 0
POL(U31(x₁, x₂)) = 1 + x₁ + x₂
POL(U31ACTIVE(x₁, x₂)) = 1 + x₂
POL(U31Active(x₁, x₂)) = 0
POL(U32(x₁)) = 1 + x₁
POL(U32Active(x₁)) = 0
POL(U41(x₁, x₂, x₃)) = 1 + x₁ + x₂ + x₃
POL(U41ACTIVE(x₁, x₂, x₃)) = 1 + x₂ + x₃
POL(U41Active(x₁, x₂, x₃)) = 0
POL(U42(x₁, x₂)) = 1 + x₁ + x₂
POL(U42ACTIVE(x₁, x₂)) = 1 + x₂
POL(U42Active(x₁, x₂)) = 0
POL(U43(x₁)) = 1 + x₁
POL(U43Active(x₁)) = 0
POL(U51(x₁, x₂, x₃)) = 1 + x₁ + x₂ + x₃
POL(U51ACTIVE(x₁, x₂, x₃)) = 1 + x₂ + x₃
POL(U51Active(x₁, x₂, x₃)) = 0
POL(U52(x₁, x₂)) = 1 + x₁ + x₂
POL(U52ACTIVE(x₁, x₂)) = 1 + x₂
POL(U52Active(x₁, x₂)) = 0
POL(U53(x₁)) = 1 + x₁
POL(U53Active(x₁)) = 0
POL(U61(x₁, x₂)) = 0
POL(U61Active(x₁, x₂)) = 0
POL(and(x₁, x₂)) = 1 + x₁ + x₂
POL(andActive(x₁, x₂)) = 0
POL(cons(x₁, x₂)) = 1 + x₁ + x₂
POL(isNat(x₁)) = x₁
POL(isNatActive(x₁)) = 0
POL(isNatIList(x₁)) = 1 + x₁
POL(isNatIListActive(x₁)) = 0
POL(isNatIListKind(x₁)) = 1 + x₁
POL(isNatIListKindActive(x₁)) = 0
POL(isNatKind(x₁)) = 1 + x₁
POL(isNatKindActive(x₁)) = 0
POL(isNatList(x₁)) = 1 + x₁
POL(isNatListActive(x₁)) = 0
POL(length(x₁)) = 1 + x₁
POL(lengthActive(x₁)) = 0
POL(mark(x₁)) = 0
POL(nil) = 0
POL(s(x₁)) = 1 + x₁
POL(tt) = 0
POL(zeros) = 0
POL(zerosActive) = 0

The following usable rules [17] were oriented: none

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ DependencyGraphProof

                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ISNATACTIVE(length(V1)) → ISNATILISTKINDACTIVE(V1)
ISNATACTIVE(s(V1)) → U21ACTIVE(isNatKindActive(V1), V1)
U51ACTIVE(tt, V1, V2) → U52ACTIVE(isNatActive(V1), V2)
ISNATILISTACTIVE(V) → U31ACTIVE(isNatIListKindActive(V), V)
U11ACTIVE(tt, V1) → ISNATLISTACTIVE(V1)
ANDACTIVE(tt, X) → MARK(X)
ISNATACTIVE(length(V1)) → U11ACTIVE(isNatIListKindActive(V1), V1)
ISNATACTIVE(s(V1)) → ISNATKINDACTIVE(V1)
U31ACTIVE(tt, V) → ISNATLISTACTIVE(V)
ISNATILISTKINDACTIVE(cons(V1, V2)) → ANDACTIVE(isNatKindActive(V1), isNatIListKind(V2))
ISNATILISTACTIVE(cons(V1, V2)) → ANDACTIVE(isNatKindActive(V1), isNatIListKind(V2))
ISNATLISTACTIVE(cons(V1, V2)) → ANDACTIVE(isNatKindActive(V1), isNatIListKind(V2))
U42ACTIVE(tt, V2) → ISNATILISTACTIVE(V2)
U52ACTIVE(tt, V2) → ISNATLISTACTIVE(V2)
ISNATILISTACTIVE(V) → ISNATILISTKINDACTIVE(V)
U41ACTIVE(tt, V1, V2) → U42ACTIVE(isNatActive(V1), V2)

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U12(x1)) → U12Active(mark(x1))
U12Active(x1) → U12(x1)
mark(U21(x1, x2)) → U21Active(mark(x1), x2)
U21Active(x1, x2) → U21(x1, x2)
mark(U22(x1)) → U22Active(mark(x1))
U22Active(x1) → U22(x1)
mark(U31(x1, x2)) → U31Active(mark(x1), x2)
U31Active(x1, x2) → U31(x1, x2)
mark(U32(x1)) → U32Active(mark(x1))
U32Active(x1) → U32(x1)
mark(U41(x1, x2, x3)) → U41Active(mark(x1), x2, x3)
U41Active(x1, x2, x3) → U41(x1, x2, x3)
mark(U42(x1, x2)) → U42Active(mark(x1), x2)
U42Active(x1, x2) → U42(x1, x2)
mark(U43(x1)) → U43Active(mark(x1))
U43Active(x1) → U43(x1)
mark(U51(x1, x2, x3)) → U51Active(mark(x1), x2, x3)
U51Active(x1, x2, x3) → U51(x1, x2, x3)
mark(U52(x1, x2)) → U52Active(mark(x1), x2)
U52Active(x1, x2) → U52(x1, x2)
mark(U53(x1)) → U53Active(mark(x1))
U53Active(x1) → U53(x1)
mark(U61(x1, x2)) → U61Active(mark(x1), x2)
U61Active(x1, x2) → U61(x1, x2)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatIListKind(x1)) → isNatIListKindActive(x1)
isNatIListKindActive(x1) → isNatIListKind(x1)
mark(isNatKind(x1)) → isNatKindActive(x1)
isNatKindActive(x1) → isNatKind(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, V1) → U12Active(isNatListActive(V1))
U12Active(tt) → tt
U21Active(tt, V1) → U22Active(isNatActive(V1))
U22Active(tt) → tt
U31Active(tt, V) → U32Active(isNatListActive(V))
U32Active(tt) → tt
U41Active(tt, V1, V2) → U42Active(isNatActive(V1), V2)
U42Active(tt, V2) → U43Active(isNatIListActive(V2))
U43Active(tt) → tt
U51Active(tt, V1, V2) → U52Active(isNatActive(V1), V2)
U52Active(tt, V2) → U53Active(isNatListActive(V2))
U53Active(tt) → tt
U61Active(tt, L) → s(lengthActive(mark(L)))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → U11Active(isNatIListKindActive(V1), V1)
isNatActive(s(V1)) → U21Active(isNatKindActive(V1), V1)
isNatIListActive(V) → U31Active(isNatIListKindActive(V), V)
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → U41Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
isNatIListKindActive(nil) → tt
isNatIListKindActive(zeros) → tt
isNatIListKindActive(cons(V1, V2)) → andActive(isNatKindActive(V1), isNatIListKind(V2))
isNatKindActive(0) → tt
isNatKindActive(length(V1)) → isNatIListKindActive(V1)
isNatKindActive(s(V1)) → isNatKindActive(V1)
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → U51Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U61Active(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 16 less nodes.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

U61ACTIVE(tt, L) → LENGTHACTIVE(mark(L))
LENGTHACTIVE(cons(N, L)) → U61ACTIVE(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U12(x1)) → U12Active(mark(x1))
U12Active(x1) → U12(x1)
mark(U21(x1, x2)) → U21Active(mark(x1), x2)
U21Active(x1, x2) → U21(x1, x2)
mark(U22(x1)) → U22Active(mark(x1))
U22Active(x1) → U22(x1)
mark(U31(x1, x2)) → U31Active(mark(x1), x2)
U31Active(x1, x2) → U31(x1, x2)
mark(U32(x1)) → U32Active(mark(x1))
U32Active(x1) → U32(x1)
mark(U41(x1, x2, x3)) → U41Active(mark(x1), x2, x3)
U41Active(x1, x2, x3) → U41(x1, x2, x3)
mark(U42(x1, x2)) → U42Active(mark(x1), x2)
U42Active(x1, x2) → U42(x1, x2)
mark(U43(x1)) → U43Active(mark(x1))
U43Active(x1) → U43(x1)
mark(U51(x1, x2, x3)) → U51Active(mark(x1), x2, x3)
U51Active(x1, x2, x3) → U51(x1, x2, x3)
mark(U52(x1, x2)) → U52Active(mark(x1), x2)
U52Active(x1, x2) → U52(x1, x2)
mark(U53(x1)) → U53Active(mark(x1))
U53Active(x1) → U53(x1)
mark(U61(x1, x2)) → U61Active(mark(x1), x2)
U61Active(x1, x2) → U61(x1, x2)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatIListKind(x1)) → isNatIListKindActive(x1)
isNatIListKindActive(x1) → isNatIListKind(x1)
mark(isNatKind(x1)) → isNatKindActive(x1)
isNatKindActive(x1) → isNatKind(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, V1) → U12Active(isNatListActive(V1))
U12Active(tt) → tt
U21Active(tt, V1) → U22Active(isNatActive(V1))
U22Active(tt) → tt
U31Active(tt, V) → U32Active(isNatListActive(V))
U32Active(tt) → tt
U41Active(tt, V1, V2) → U42Active(isNatActive(V1), V2)
U42Active(tt, V2) → U43Active(isNatIListActive(V2))
U43Active(tt) → tt
U51Active(tt, V1, V2) → U52Active(isNatActive(V1), V2)
U52Active(tt, V2) → U53Active(isNatListActive(V2))
U53Active(tt) → tt
U61Active(tt, L) → s(lengthActive(mark(L)))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → U11Active(isNatIListKindActive(V1), V1)
isNatActive(s(V1)) → U21Active(isNatKindActive(V1), V1)
isNatIListActive(V) → U31Active(isNatIListKindActive(V), V)
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → U41Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
isNatIListKindActive(nil) → tt
isNatIListKindActive(zeros) → tt
isNatIListKindActive(cons(V1, V2)) → andActive(isNatKindActive(V1), isNatIListKind(V2))
isNatKindActive(0) → tt
isNatKindActive(length(V1)) → isNatIListKindActive(V1)
isNatKindActive(s(V1)) → isNatKindActive(V1)
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → U51Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U61Active(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule U61ACTIVE(tt, L) → LENGTHACTIVE(mark(L)) at position [0] we obtained the following new rules:

U61ACTIVE(tt, isNatIListKind(x0)) → LENGTHACTIVE(isNatIListKindActive(x0))
U61ACTIVE(tt, tt) → LENGTHACTIVE(tt)
U61ACTIVE(tt, U52(x0, x1)) → LENGTHACTIVE(U52Active(mark(x0), x1))
U61ACTIVE(tt, U51(x0, x1, x2)) → LENGTHACTIVE(U51Active(mark(x0), x1, x2))
U61ACTIVE(tt, U32(x0)) → LENGTHACTIVE(U32Active(mark(x0)))
U61ACTIVE(tt, length(x0)) → LENGTHACTIVE(lengthActive(mark(x0)))
U61ACTIVE(tt, U42(x0, x1)) → LENGTHACTIVE(U42Active(mark(x0), x1))
U61ACTIVE(tt, U11(x0, x1)) → LENGTHACTIVE(U11Active(mark(x0), x1))
U61ACTIVE(tt, U22(x0)) → LENGTHACTIVE(U22Active(mark(x0)))
U61ACTIVE(tt, U12(x0)) → LENGTHACTIVE(U12Active(mark(x0)))
U61ACTIVE(tt, U31(x0, x1)) → LENGTHACTIVE(U31Active(mark(x0), x1))
U61ACTIVE(tt, and(x0, x1)) → LENGTHACTIVE(andActive(mark(x0), x1))
U61ACTIVE(tt, isNatIList(x0)) → LENGTHACTIVE(isNatIListActive(x0))
U61ACTIVE(tt, U43(x0)) → LENGTHACTIVE(U43Active(mark(x0)))
U61ACTIVE(tt, U61(x0, x1)) → LENGTHACTIVE(U61Active(mark(x0), x1))
U61ACTIVE(tt, s(x0)) → LENGTHACTIVE(s(mark(x0)))
U61ACTIVE(tt, U41(x0, x1, x2)) → LENGTHACTIVE(U41Active(mark(x0), x1, x2))
U61ACTIVE(tt, isNatKind(x0)) → LENGTHACTIVE(isNatKindActive(x0))
U61ACTIVE(tt, 0) → LENGTHACTIVE(0)
U61ACTIVE(tt, U21(x0, x1)) → LENGTHACTIVE(U21Active(mark(x0), x1))
U61ACTIVE(tt, zeros) → LENGTHACTIVE(zerosActive)
U61ACTIVE(tt, cons(x0, x1)) → LENGTHACTIVE(cons(mark(x0), x1))
U61ACTIVE(tt, U53(x0)) → LENGTHACTIVE(U53Active(mark(x0)))
U61ACTIVE(tt, isNat(x0)) → LENGTHACTIVE(isNatActive(x0))
U61ACTIVE(tt, isNatList(x0)) → LENGTHACTIVE(isNatListActive(x0))
U61ACTIVE(tt, nil) → LENGTHACTIVE(nil)

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

U61ACTIVE(tt, isNatIListKind(x0)) → LENGTHACTIVE(isNatIListKindActive(x0))
U61ACTIVE(tt, tt) → LENGTHACTIVE(tt)
U61ACTIVE(tt, U52(x0, x1)) → LENGTHACTIVE(U52Active(mark(x0), x1))
U61ACTIVE(tt, U51(x0, x1, x2)) → LENGTHACTIVE(U51Active(mark(x0), x1, x2))
U61ACTIVE(tt, length(x0)) → LENGTHACTIVE(lengthActive(mark(x0)))
U61ACTIVE(tt, U32(x0)) → LENGTHACTIVE(U32Active(mark(x0)))
U61ACTIVE(tt, U11(x0, x1)) → LENGTHACTIVE(U11Active(mark(x0), x1))
U61ACTIVE(tt, U42(x0, x1)) → LENGTHACTIVE(U42Active(mark(x0), x1))
U61ACTIVE(tt, U22(x0)) → LENGTHACTIVE(U22Active(mark(x0)))
U61ACTIVE(tt, U31(x0, x1)) → LENGTHACTIVE(U31Active(mark(x0), x1))
U61ACTIVE(tt, U12(x0)) → LENGTHACTIVE(U12Active(mark(x0)))
U61ACTIVE(tt, and(x0, x1)) → LENGTHACTIVE(andActive(mark(x0), x1))
U61ACTIVE(tt, isNatIList(x0)) → LENGTHACTIVE(isNatIListActive(x0))
U61ACTIVE(tt, U43(x0)) → LENGTHACTIVE(U43Active(mark(x0)))
U61ACTIVE(tt, U61(x0, x1)) → LENGTHACTIVE(U61Active(mark(x0), x1))
U61ACTIVE(tt, s(x0)) → LENGTHACTIVE(s(mark(x0)))
U61ACTIVE(tt, U41(x0, x1, x2)) → LENGTHACTIVE(U41Active(mark(x0), x1, x2))
U61ACTIVE(tt, isNatKind(x0)) → LENGTHACTIVE(isNatKindActive(x0))
U61ACTIVE(tt, 0) → LENGTHACTIVE(0)
LENGTHACTIVE(cons(N, L)) → U61ACTIVE(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)
U61ACTIVE(tt, U21(x0, x1)) → LENGTHACTIVE(U21Active(mark(x0), x1))
U61ACTIVE(tt, zeros) → LENGTHACTIVE(zerosActive)
U61ACTIVE(tt, cons(x0, x1)) → LENGTHACTIVE(cons(mark(x0), x1))
U61ACTIVE(tt, U53(x0)) → LENGTHACTIVE(U53Active(mark(x0)))
U61ACTIVE(tt, isNatList(x0)) → LENGTHACTIVE(isNatListActive(x0))
U61ACTIVE(tt, isNat(x0)) → LENGTHACTIVE(isNatActive(x0))
U61ACTIVE(tt, nil) → LENGTHACTIVE(nil)

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U12(x1)) → U12Active(mark(x1))
U12Active(x1) → U12(x1)
mark(U21(x1, x2)) → U21Active(mark(x1), x2)
U21Active(x1, x2) → U21(x1, x2)
mark(U22(x1)) → U22Active(mark(x1))
U22Active(x1) → U22(x1)
mark(U31(x1, x2)) → U31Active(mark(x1), x2)
U31Active(x1, x2) → U31(x1, x2)
mark(U32(x1)) → U32Active(mark(x1))
U32Active(x1) → U32(x1)
mark(U41(x1, x2, x3)) → U41Active(mark(x1), x2, x3)
U41Active(x1, x2, x3) → U41(x1, x2, x3)
mark(U42(x1, x2)) → U42Active(mark(x1), x2)
U42Active(x1, x2) → U42(x1, x2)
mark(U43(x1)) → U43Active(mark(x1))
U43Active(x1) → U43(x1)
mark(U51(x1, x2, x3)) → U51Active(mark(x1), x2, x3)
U51Active(x1, x2, x3) → U51(x1, x2, x3)
mark(U52(x1, x2)) → U52Active(mark(x1), x2)
U52Active(x1, x2) → U52(x1, x2)
mark(U53(x1)) → U53Active(mark(x1))
U53Active(x1) → U53(x1)
mark(U61(x1, x2)) → U61Active(mark(x1), x2)
U61Active(x1, x2) → U61(x1, x2)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatIListKind(x1)) → isNatIListKindActive(x1)
isNatIListKindActive(x1) → isNatIListKind(x1)
mark(isNatKind(x1)) → isNatKindActive(x1)
isNatKindActive(x1) → isNatKind(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, V1) → U12Active(isNatListActive(V1))
U12Active(tt) → tt
U21Active(tt, V1) → U22Active(isNatActive(V1))
U22Active(tt) → tt
U31Active(tt, V) → U32Active(isNatListActive(V))
U32Active(tt) → tt
U41Active(tt, V1, V2) → U42Active(isNatActive(V1), V2)
U42Active(tt, V2) → U43Active(isNatIListActive(V2))
U43Active(tt) → tt
U51Active(tt, V1, V2) → U52Active(isNatActive(V1), V2)
U52Active(tt, V2) → U53Active(isNatListActive(V2))
U53Active(tt) → tt
U61Active(tt, L) → s(lengthActive(mark(L)))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → U11Active(isNatIListKindActive(V1), V1)
isNatActive(s(V1)) → U21Active(isNatKindActive(V1), V1)
isNatIListActive(V) → U31Active(isNatIListKindActive(V), V)
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → U41Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
isNatIListKindActive(nil) → tt
isNatIListKindActive(zeros) → tt
isNatIListKindActive(cons(V1, V2)) → andActive(isNatKindActive(V1), isNatIListKind(V2))
isNatKindActive(0) → tt
isNatKindActive(length(V1)) → isNatIListKindActive(V1)
isNatKindActive(s(V1)) → isNatKindActive(V1)
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → U51Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U61Active(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 4 less nodes.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

U61ACTIVE(tt, isNatIListKind(x0)) → LENGTHACTIVE(isNatIListKindActive(x0))
U61ACTIVE(tt, isNatKind(x0)) → LENGTHACTIVE(isNatKindActive(x0))
U61ACTIVE(tt, U52(x0, x1)) → LENGTHACTIVE(U52Active(mark(x0), x1))
U61ACTIVE(tt, U51(x0, x1, x2)) → LENGTHACTIVE(U51Active(mark(x0), x1, x2))
U61ACTIVE(tt, U32(x0)) → LENGTHACTIVE(U32Active(mark(x0)))
U61ACTIVE(tt, length(x0)) → LENGTHACTIVE(lengthActive(mark(x0)))
LENGTHACTIVE(cons(N, L)) → U61ACTIVE(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)
U61ACTIVE(tt, U21(x0, x1)) → LENGTHACTIVE(U21Active(mark(x0), x1))
U61ACTIVE(tt, U42(x0, x1)) → LENGTHACTIVE(U42Active(mark(x0), x1))
U61ACTIVE(tt, U11(x0, x1)) → LENGTHACTIVE(U11Active(mark(x0), x1))
U61ACTIVE(tt, U22(x0)) → LENGTHACTIVE(U22Active(mark(x0)))
U61ACTIVE(tt, U12(x0)) → LENGTHACTIVE(U12Active(mark(x0)))
U61ACTIVE(tt, U31(x0, x1)) → LENGTHACTIVE(U31Active(mark(x0), x1))
U61ACTIVE(tt, and(x0, x1)) → LENGTHACTIVE(andActive(mark(x0), x1))
U61ACTIVE(tt, isNatIList(x0)) → LENGTHACTIVE(isNatIListActive(x0))
U61ACTIVE(tt, cons(x0, x1)) → LENGTHACTIVE(cons(mark(x0), x1))
U61ACTIVE(tt, zeros) → LENGTHACTIVE(zerosActive)
U61ACTIVE(tt, U61(x0, x1)) → LENGTHACTIVE(U61Active(mark(x0), x1))
U61ACTIVE(tt, U43(x0)) → LENGTHACTIVE(U43Active(mark(x0)))
U61ACTIVE(tt, U53(x0)) → LENGTHACTIVE(U53Active(mark(x0)))
U61ACTIVE(tt, U41(x0, x1, x2)) → LENGTHACTIVE(U41Active(mark(x0), x1, x2))
U61ACTIVE(tt, isNatList(x0)) → LENGTHACTIVE(isNatListActive(x0))
U61ACTIVE(tt, isNat(x0)) → LENGTHACTIVE(isNatActive(x0))

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U12(x1)) → U12Active(mark(x1))
U12Active(x1) → U12(x1)
mark(U21(x1, x2)) → U21Active(mark(x1), x2)
U21Active(x1, x2) → U21(x1, x2)
mark(U22(x1)) → U22Active(mark(x1))
U22Active(x1) → U22(x1)
mark(U31(x1, x2)) → U31Active(mark(x1), x2)
U31Active(x1, x2) → U31(x1, x2)
mark(U32(x1)) → U32Active(mark(x1))
U32Active(x1) → U32(x1)
mark(U41(x1, x2, x3)) → U41Active(mark(x1), x2, x3)
U41Active(x1, x2, x3) → U41(x1, x2, x3)
mark(U42(x1, x2)) → U42Active(mark(x1), x2)
U42Active(x1, x2) → U42(x1, x2)
mark(U43(x1)) → U43Active(mark(x1))
U43Active(x1) → U43(x1)
mark(U51(x1, x2, x3)) → U51Active(mark(x1), x2, x3)
U51Active(x1, x2, x3) → U51(x1, x2, x3)
mark(U52(x1, x2)) → U52Active(mark(x1), x2)
U52Active(x1, x2) → U52(x1, x2)
mark(U53(x1)) → U53Active(mark(x1))
U53Active(x1) → U53(x1)
mark(U61(x1, x2)) → U61Active(mark(x1), x2)
U61Active(x1, x2) → U61(x1, x2)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatIListKind(x1)) → isNatIListKindActive(x1)
isNatIListKindActive(x1) → isNatIListKind(x1)
mark(isNatKind(x1)) → isNatKindActive(x1)
isNatKindActive(x1) → isNatKind(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, V1) → U12Active(isNatListActive(V1))
U12Active(tt) → tt
U21Active(tt, V1) → U22Active(isNatActive(V1))
U22Active(tt) → tt
U31Active(tt, V) → U32Active(isNatListActive(V))
U32Active(tt) → tt
U41Active(tt, V1, V2) → U42Active(isNatActive(V1), V2)
U42Active(tt, V2) → U43Active(isNatIListActive(V2))
U43Active(tt) → tt
U51Active(tt, V1, V2) → U52Active(isNatActive(V1), V2)
U52Active(tt, V2) → U53Active(isNatListActive(V2))
U53Active(tt) → tt
U61Active(tt, L) → s(lengthActive(mark(L)))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → U11Active(isNatIListKindActive(V1), V1)
isNatActive(s(V1)) → U21Active(isNatKindActive(V1), V1)
isNatIListActive(V) → U31Active(isNatIListKindActive(V), V)
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → U41Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
isNatIListKindActive(nil) → tt
isNatIListKindActive(zeros) → tt
isNatIListKindActive(cons(V1, V2)) → andActive(isNatKindActive(V1), isNatIListKind(V2))
isNatKindActive(0) → tt
isNatKindActive(length(V1)) → isNatIListKindActive(V1)
isNatKindActive(s(V1)) → isNatKindActive(V1)
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → U51Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U61Active(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule U61ACTIVE(tt, zeros) → LENGTHACTIVE(zerosActive) at position [0] we obtained the following new rules:

U61ACTIVE(tt, zeros) → LENGTHACTIVE(cons(0, zeros))
U61ACTIVE(tt, zeros) → LENGTHACTIVE(zeros)

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

U61ACTIVE(tt, isNatIListKind(x0)) → LENGTHACTIVE(isNatIListKindActive(x0))
U61ACTIVE(tt, U52(x0, x1)) → LENGTHACTIVE(U52Active(mark(x0), x1))
U61ACTIVE(tt, U51(x0, x1, x2)) → LENGTHACTIVE(U51Active(mark(x0), x1, x2))
U61ACTIVE(tt, U32(x0)) → LENGTHACTIVE(U32Active(mark(x0)))
U61ACTIVE(tt, length(x0)) → LENGTHACTIVE(lengthActive(mark(x0)))
U61ACTIVE(tt, U42(x0, x1)) → LENGTHACTIVE(U42Active(mark(x0), x1))
U61ACTIVE(tt, U11(x0, x1)) → LENGTHACTIVE(U11Active(mark(x0), x1))
U61ACTIVE(tt, U22(x0)) → LENGTHACTIVE(U22Active(mark(x0)))
U61ACTIVE(tt, U12(x0)) → LENGTHACTIVE(U12Active(mark(x0)))
U61ACTIVE(tt, U31(x0, x1)) → LENGTHACTIVE(U31Active(mark(x0), x1))
U61ACTIVE(tt, and(x0, x1)) → LENGTHACTIVE(andActive(mark(x0), x1))
U61ACTIVE(tt, isNatIList(x0)) → LENGTHACTIVE(isNatIListActive(x0))
U61ACTIVE(tt, U61(x0, x1)) → LENGTHACTIVE(U61Active(mark(x0), x1))
U61ACTIVE(tt, U43(x0)) → LENGTHACTIVE(U43Active(mark(x0)))
U61ACTIVE(tt, U41(x0, x1, x2)) → LENGTHACTIVE(U41Active(mark(x0), x1, x2))
U61ACTIVE(tt, isNatKind(x0)) → LENGTHACTIVE(isNatKindActive(x0))
U61ACTIVE(tt, zeros) → LENGTHACTIVE(cons(0, zeros))
LENGTHACTIVE(cons(N, L)) → U61ACTIVE(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)
U61ACTIVE(tt, U21(x0, x1)) → LENGTHACTIVE(U21Active(mark(x0), x1))
U61ACTIVE(tt, zeros) → LENGTHACTIVE(zeros)
U61ACTIVE(tt, cons(x0, x1)) → LENGTHACTIVE(cons(mark(x0), x1))
U61ACTIVE(tt, U53(x0)) → LENGTHACTIVE(U53Active(mark(x0)))
U61ACTIVE(tt, isNatList(x0)) → LENGTHACTIVE(isNatListActive(x0))
U61ACTIVE(tt, isNat(x0)) → LENGTHACTIVE(isNatActive(x0))

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U12(x1)) → U12Active(mark(x1))
U12Active(x1) → U12(x1)
mark(U21(x1, x2)) → U21Active(mark(x1), x2)
U21Active(x1, x2) → U21(x1, x2)
mark(U22(x1)) → U22Active(mark(x1))
U22Active(x1) → U22(x1)
mark(U31(x1, x2)) → U31Active(mark(x1), x2)
U31Active(x1, x2) → U31(x1, x2)
mark(U32(x1)) → U32Active(mark(x1))
U32Active(x1) → U32(x1)
mark(U41(x1, x2, x3)) → U41Active(mark(x1), x2, x3)
U41Active(x1, x2, x3) → U41(x1, x2, x3)
mark(U42(x1, x2)) → U42Active(mark(x1), x2)
U42Active(x1, x2) → U42(x1, x2)
mark(U43(x1)) → U43Active(mark(x1))
U43Active(x1) → U43(x1)
mark(U51(x1, x2, x3)) → U51Active(mark(x1), x2, x3)
U51Active(x1, x2, x3) → U51(x1, x2, x3)
mark(U52(x1, x2)) → U52Active(mark(x1), x2)
U52Active(x1, x2) → U52(x1, x2)
mark(U53(x1)) → U53Active(mark(x1))
U53Active(x1) → U53(x1)
mark(U61(x1, x2)) → U61Active(mark(x1), x2)
U61Active(x1, x2) → U61(x1, x2)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatIListKind(x1)) → isNatIListKindActive(x1)
isNatIListKindActive(x1) → isNatIListKind(x1)
mark(isNatKind(x1)) → isNatKindActive(x1)
isNatKindActive(x1) → isNatKind(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, V1) → U12Active(isNatListActive(V1))
U12Active(tt) → tt
U21Active(tt, V1) → U22Active(isNatActive(V1))
U22Active(tt) → tt
U31Active(tt, V) → U32Active(isNatListActive(V))
U32Active(tt) → tt
U41Active(tt, V1, V2) → U42Active(isNatActive(V1), V2)
U42Active(tt, V2) → U43Active(isNatIListActive(V2))
U43Active(tt) → tt
U51Active(tt, V1, V2) → U52Active(isNatActive(V1), V2)
U52Active(tt, V2) → U53Active(isNatListActive(V2))
U53Active(tt) → tt
U61Active(tt, L) → s(lengthActive(mark(L)))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → U11Active(isNatIListKindActive(V1), V1)
isNatActive(s(V1)) → U21Active(isNatKindActive(V1), V1)
isNatIListActive(V) → U31Active(isNatIListKindActive(V), V)
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → U41Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
isNatIListKindActive(nil) → tt
isNatIListKindActive(zeros) → tt
isNatIListKindActive(cons(V1, V2)) → andActive(isNatKindActive(V1), isNatIListKind(V2))
isNatKindActive(0) → tt
isNatKindActive(length(V1)) → isNatIListKindActive(V1)
isNatKindActive(s(V1)) → isNatKindActive(V1)
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → U51Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U61Active(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ QDP

                                        ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

U61ACTIVE(tt, isNatIListKind(x0)) → LENGTHACTIVE(isNatIListKindActive(x0))
U61ACTIVE(tt, isNatKind(x0)) → LENGTHACTIVE(isNatKindActive(x0))
U61ACTIVE(tt, zeros) → LENGTHACTIVE(cons(0, zeros))
U61ACTIVE(tt, U52(x0, x1)) → LENGTHACTIVE(U52Active(mark(x0), x1))
U61ACTIVE(tt, U51(x0, x1, x2)) → LENGTHACTIVE(U51Active(mark(x0), x1, x2))
U61ACTIVE(tt, U32(x0)) → LENGTHACTIVE(U32Active(mark(x0)))
U61ACTIVE(tt, length(x0)) → LENGTHACTIVE(lengthActive(mark(x0)))
LENGTHACTIVE(cons(N, L)) → U61ACTIVE(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)
U61ACTIVE(tt, U21(x0, x1)) → LENGTHACTIVE(U21Active(mark(x0), x1))
U61ACTIVE(tt, U42(x0, x1)) → LENGTHACTIVE(U42Active(mark(x0), x1))
U61ACTIVE(tt, U11(x0, x1)) → LENGTHACTIVE(U11Active(mark(x0), x1))
U61ACTIVE(tt, U22(x0)) → LENGTHACTIVE(U22Active(mark(x0)))
U61ACTIVE(tt, U12(x0)) → LENGTHACTIVE(U12Active(mark(x0)))
U61ACTIVE(tt, U31(x0, x1)) → LENGTHACTIVE(U31Active(mark(x0), x1))
U61ACTIVE(tt, and(x0, x1)) → LENGTHACTIVE(andActive(mark(x0), x1))
U61ACTIVE(tt, isNatIList(x0)) → LENGTHACTIVE(isNatIListActive(x0))
U61ACTIVE(tt, cons(x0, x1)) → LENGTHACTIVE(cons(mark(x0), x1))
U61ACTIVE(tt, U61(x0, x1)) → LENGTHACTIVE(U61Active(mark(x0), x1))
U61ACTIVE(tt, U43(x0)) → LENGTHACTIVE(U43Active(mark(x0)))
U61ACTIVE(tt, U53(x0)) → LENGTHACTIVE(U53Active(mark(x0)))
U61ACTIVE(tt, U41(x0, x1, x2)) → LENGTHACTIVE(U41Active(mark(x0), x1, x2))
U61ACTIVE(tt, isNatList(x0)) → LENGTHACTIVE(isNatListActive(x0))
U61ACTIVE(tt, isNat(x0)) → LENGTHACTIVE(isNatActive(x0))

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U12(x1)) → U12Active(mark(x1))
U12Active(x1) → U12(x1)
mark(U21(x1, x2)) → U21Active(mark(x1), x2)
U21Active(x1, x2) → U21(x1, x2)
mark(U22(x1)) → U22Active(mark(x1))
U22Active(x1) → U22(x1)
mark(U31(x1, x2)) → U31Active(mark(x1), x2)
U31Active(x1, x2) → U31(x1, x2)
mark(U32(x1)) → U32Active(mark(x1))
U32Active(x1) → U32(x1)
mark(U41(x1, x2, x3)) → U41Active(mark(x1), x2, x3)
U41Active(x1, x2, x3) → U41(x1, x2, x3)
mark(U42(x1, x2)) → U42Active(mark(x1), x2)
U42Active(x1, x2) → U42(x1, x2)
mark(U43(x1)) → U43Active(mark(x1))
U43Active(x1) → U43(x1)
mark(U51(x1, x2, x3)) → U51Active(mark(x1), x2, x3)
U51Active(x1, x2, x3) → U51(x1, x2, x3)
mark(U52(x1, x2)) → U52Active(mark(x1), x2)
U52Active(x1, x2) → U52(x1, x2)
mark(U53(x1)) → U53Active(mark(x1))
U53Active(x1) → U53(x1)
mark(U61(x1, x2)) → U61Active(mark(x1), x2)
U61Active(x1, x2) → U61(x1, x2)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatIListKind(x1)) → isNatIListKindActive(x1)
isNatIListKindActive(x1) → isNatIListKind(x1)
mark(isNatKind(x1)) → isNatKindActive(x1)
isNatKindActive(x1) → isNatKind(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, V1) → U12Active(isNatListActive(V1))
U12Active(tt) → tt
U21Active(tt, V1) → U22Active(isNatActive(V1))
U22Active(tt) → tt
U31Active(tt, V) → U32Active(isNatListActive(V))
U32Active(tt) → tt
U41Active(tt, V1, V2) → U42Active(isNatActive(V1), V2)
U42Active(tt, V2) → U43Active(isNatIListActive(V2))
U43Active(tt) → tt
U51Active(tt, V1, V2) → U52Active(isNatActive(V1), V2)
U52Active(tt, V2) → U53Active(isNatListActive(V2))
U53Active(tt) → tt
U61Active(tt, L) → s(lengthActive(mark(L)))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → U11Active(isNatIListKindActive(V1), V1)
isNatActive(s(V1)) → U21Active(isNatKindActive(V1), V1)
isNatIListActive(V) → U31Active(isNatIListKindActive(V), V)
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → U41Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
isNatIListKindActive(nil) → tt
isNatIListKindActive(zeros) → tt
isNatIListKindActive(cons(V1, V2)) → andActive(isNatKindActive(V1), isNatIListKind(V2))
isNatKindActive(0) → tt
isNatKindActive(length(V1)) → isNatIListKindActive(V1)
isNatKindActive(s(V1)) → isNatKindActive(V1)
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → U51Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U61Active(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

U61ACTIVE(tt, length(x0)) → LENGTHACTIVE(lengthActive(mark(x0)))
U61ACTIVE(tt, U61(x0, x1)) → LENGTHACTIVE(U61Active(mark(x0), x1))

The remaining pairs can at least be oriented weakly.

U61ACTIVE(tt, isNatIListKind(x0)) → LENGTHACTIVE(isNatIListKindActive(x0))
U61ACTIVE(tt, isNatKind(x0)) → LENGTHACTIVE(isNatKindActive(x0))
U61ACTIVE(tt, zeros) → LENGTHACTIVE(cons(0, zeros))
U61ACTIVE(tt, U52(x0, x1)) → LENGTHACTIVE(U52Active(mark(x0), x1))
U61ACTIVE(tt, U51(x0, x1, x2)) → LENGTHACTIVE(U51Active(mark(x0), x1, x2))
U61ACTIVE(tt, U32(x0)) → LENGTHACTIVE(U32Active(mark(x0)))
LENGTHACTIVE(cons(N, L)) → U61ACTIVE(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)
U61ACTIVE(tt, U21(x0, x1)) → LENGTHACTIVE(U21Active(mark(x0), x1))
U61ACTIVE(tt, U42(x0, x1)) → LENGTHACTIVE(U42Active(mark(x0), x1))
U61ACTIVE(tt, U11(x0, x1)) → LENGTHACTIVE(U11Active(mark(x0), x1))
U61ACTIVE(tt, U22(x0)) → LENGTHACTIVE(U22Active(mark(x0)))
U61ACTIVE(tt, U12(x0)) → LENGTHACTIVE(U12Active(mark(x0)))
U61ACTIVE(tt, U31(x0, x1)) → LENGTHACTIVE(U31Active(mark(x0), x1))
U61ACTIVE(tt, and(x0, x1)) → LENGTHACTIVE(andActive(mark(x0), x1))
U61ACTIVE(tt, isNatIList(x0)) → LENGTHACTIVE(isNatIListActive(x0))
U61ACTIVE(tt, cons(x0, x1)) → LENGTHACTIVE(cons(mark(x0), x1))
U61ACTIVE(tt, U43(x0)) → LENGTHACTIVE(U43Active(mark(x0)))
U61ACTIVE(tt, U53(x0)) → LENGTHACTIVE(U53Active(mark(x0)))
U61ACTIVE(tt, U41(x0, x1, x2)) → LENGTHACTIVE(U41Active(mark(x0), x1, x2))
U61ACTIVE(tt, isNatList(x0)) → LENGTHACTIVE(isNatListActive(x0))
U61ACTIVE(tt, isNat(x0)) → LENGTHACTIVE(isNatActive(x0))

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(LENGTHACTIVE(x₁)) = x₁
POL(U11(x₁, x₂)) = 0
POL(U11Active(x₁, x₂)) = 1
POL(U12(x₁)) = 0
POL(U12Active(x₁)) = 1
POL(U21(x₁, x₂)) = 0
POL(U21Active(x₁, x₂)) = 1
POL(U22(x₁)) = 0
POL(U22Active(x₁)) = 1
POL(U31(x₁, x₂)) = 0
POL(U31Active(x₁, x₂)) = 1
POL(U32(x₁)) = 0
POL(U32Active(x₁)) = 1
POL(U41(x₁, x₂, x₃)) = 0
POL(U41Active(x₁, x₂, x₃)) = 1
POL(U42(x₁, x₂)) = 0
POL(U42Active(x₁, x₂)) = 1
POL(U43(x₁)) = 0
POL(U43Active(x₁)) = 1
POL(U51(x₁, x₂, x₃)) = 1
POL(U51Active(x₁, x₂, x₃)) = 1
POL(U52(x₁, x₂)) = x₁
POL(U52Active(x₁, x₂)) = x₁
POL(U53(x₁)) = 0
POL(U53Active(x₁)) = 1
POL(U61(x₁, x₂)) = 0
POL(U61ACTIVE(x₁, x₂)) = x₁
POL(U61Active(x₁, x₂)) = 0
POL(and(x₁, x₂)) = 0
POL(andActive(x₁, x₂)) = x₁
POL(cons(x₁, x₂)) = 1
POL(isNat(x₁)) = 0
POL(isNatActive(x₁)) = 1
POL(isNatIList(x₁)) = 0
POL(isNatIListActive(x₁)) = 1
POL(isNatIListKind(x₁)) = 0
POL(isNatIListKindActive(x₁)) = 1
POL(isNatKind(x₁)) = 0
POL(isNatKindActive(x₁)) = 1
POL(isNatList(x₁)) = 0
POL(isNatListActive(x₁)) = 1
POL(length(x₁)) = 0
POL(lengthActive(x₁)) = 0
POL(mark(x₁)) = 1
POL(nil) = 0
POL(s(x₁)) = 0
POL(tt) = 1
POL(zeros) = 0
POL(zerosActive) = 1

The following usable rules [17] were oriented:

isNatKindActive(0) → tt
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → U41Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
mark(zeros) → zerosActive
isNatIListKindActive(nil) → tt
zerosActive → zeros
isNatIListKindActive(zeros) → tt
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → U51Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U61Active(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
isNatKindActive(length(V1)) → isNatIListKindActive(V1)
isNatIListKindActive(cons(V1, V2)) → andActive(isNatKindActive(V1), isNatIListKind(V2))
mark(isNatKind(x1)) → isNatKindActive(x1)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(tt, X) → mark(X)
mark(isNatIListKind(x1)) → isNatIListKindActive(x1)
isNatKindActive(s(V1)) → isNatKindActive(V1)
andActive(x1, x2) → and(x1, x2)
mark(U61(x1, x2)) → U61Active(mark(x1), x2)
U61Active(x1, x2) → U61(x1, x2)
mark(U53(x1)) → U53Active(mark(x1))
U53Active(x1) → U53(x1)
mark(U52(x1, x2)) → U52Active(mark(x1), x2)
U52Active(x1, x2) → U52(x1, x2)
mark(U51(x1, x2, x3)) → U51Active(mark(x1), x2, x3)
U51Active(x1, x2, x3) → U51(x1, x2, x3)
mark(U43(x1)) → U43Active(mark(x1))
U43Active(x1) → U43(x1)
U42Active(x1, x2) → U42(x1, x2)
mark(U42(x1, x2)) → U42Active(mark(x1), x2)
U41Active(x1, x2, x3) → U41(x1, x2, x3)
mark(U41(x1, x2, x3)) → U41Active(mark(x1), x2, x3)
U32Active(x1) → U32(x1)
mark(U32(x1)) → U32Active(mark(x1))
U31Active(x1, x2) → U31(x1, x2)
mark(U31(x1, x2)) → U31Active(mark(x1), x2)
U22Active(x1) → U22(x1)
mark(U22(x1)) → U22Active(mark(x1))
U21Active(x1, x2) → U21(x1, x2)
mark(U21(x1, x2)) → U21Active(mark(x1), x2)
U12Active(x1) → U12(x1)
mark(U12(x1)) → U12Active(mark(x1))
U11Active(x1, x2) → U11(x1, x2)
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
isNatActive(0) → tt
isNatActive(length(V1)) → U11Active(isNatIListKindActive(V1), V1)
isNatActive(s(V1)) → U21Active(isNatKindActive(V1), V1)
isNatIListActive(V) → U31Active(isNatIListKindActive(V), V)
U52Active(tt, V2) → U53Active(isNatListActive(V2))
U53Active(tt) → tt
U61Active(tt, L) → s(lengthActive(mark(L)))
U41Active(tt, V1, V2) → U42Active(isNatActive(V1), V2)
U42Active(tt, V2) → U43Active(isNatIListActive(V2))
U43Active(tt) → tt
U51Active(tt, V1, V2) → U52Active(isNatActive(V1), V2)
U21Active(tt, V1) → U22Active(isNatActive(V1))
U22Active(tt) → tt
U31Active(tt, V) → U32Active(isNatListActive(V))
U32Active(tt) → tt
zerosActive → cons(0, zeros)
mark(nil) → nil
U12Active(tt) → tt
U11Active(tt, V1) → U12Active(isNatListActive(V1))
mark(0) → 0
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(s(x1)) → s(mark(x1))
mark(tt) → tt
isNatListActive(x1) → isNatList(x1)
mark(isNatList(x1)) → isNatListActive(x1)
lengthActive(x1) → length(x1)
mark(length(x1)) → lengthActive(mark(x1))
isNatIListKindActive(x1) → isNatIListKind(x1)
isNatKindActive(x1) → isNatKind(x1)

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

U61ACTIVE(tt, isNatIListKind(x0)) → LENGTHACTIVE(isNatIListKindActive(x0))
U61ACTIVE(tt, isNatKind(x0)) → LENGTHACTIVE(isNatKindActive(x0))
U61ACTIVE(tt, zeros) → LENGTHACTIVE(cons(0, zeros))
U61ACTIVE(tt, U52(x0, x1)) → LENGTHACTIVE(U52Active(mark(x0), x1))
U61ACTIVE(tt, U51(x0, x1, x2)) → LENGTHACTIVE(U51Active(mark(x0), x1, x2))
U61ACTIVE(tt, U32(x0)) → LENGTHACTIVE(U32Active(mark(x0)))
LENGTHACTIVE(cons(N, L)) → U61ACTIVE(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)
U61ACTIVE(tt, U21(x0, x1)) → LENGTHACTIVE(U21Active(mark(x0), x1))
U61ACTIVE(tt, U42(x0, x1)) → LENGTHACTIVE(U42Active(mark(x0), x1))
U61ACTIVE(tt, U11(x0, x1)) → LENGTHACTIVE(U11Active(mark(x0), x1))
U61ACTIVE(tt, U22(x0)) → LENGTHACTIVE(U22Active(mark(x0)))
U61ACTIVE(tt, U12(x0)) → LENGTHACTIVE(U12Active(mark(x0)))
U61ACTIVE(tt, U31(x0, x1)) → LENGTHACTIVE(U31Active(mark(x0), x1))
U61ACTIVE(tt, isNatIList(x0)) → LENGTHACTIVE(isNatIListActive(x0))
U61ACTIVE(tt, and(x0, x1)) → LENGTHACTIVE(andActive(mark(x0), x1))
U61ACTIVE(tt, cons(x0, x1)) → LENGTHACTIVE(cons(mark(x0), x1))
U61ACTIVE(tt, U43(x0)) → LENGTHACTIVE(U43Active(mark(x0)))
U61ACTIVE(tt, U53(x0)) → LENGTHACTIVE(U53Active(mark(x0)))
U61ACTIVE(tt, U41(x0, x1, x2)) → LENGTHACTIVE(U41Active(mark(x0), x1, x2))
U61ACTIVE(tt, isNat(x0)) → LENGTHACTIVE(isNatActive(x0))
U61ACTIVE(tt, isNatList(x0)) → LENGTHACTIVE(isNatListActive(x0))

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U12(x1)) → U12Active(mark(x1))
U12Active(x1) → U12(x1)
mark(U21(x1, x2)) → U21Active(mark(x1), x2)
U21Active(x1, x2) → U21(x1, x2)
mark(U22(x1)) → U22Active(mark(x1))
U22Active(x1) → U22(x1)
mark(U31(x1, x2)) → U31Active(mark(x1), x2)
U31Active(x1, x2) → U31(x1, x2)
mark(U32(x1)) → U32Active(mark(x1))
U32Active(x1) → U32(x1)
mark(U41(x1, x2, x3)) → U41Active(mark(x1), x2, x3)
U41Active(x1, x2, x3) → U41(x1, x2, x3)
mark(U42(x1, x2)) → U42Active(mark(x1), x2)
U42Active(x1, x2) → U42(x1, x2)
mark(U43(x1)) → U43Active(mark(x1))
U43Active(x1) → U43(x1)
mark(U51(x1, x2, x3)) → U51Active(mark(x1), x2, x3)
U51Active(x1, x2, x3) → U51(x1, x2, x3)
mark(U52(x1, x2)) → U52Active(mark(x1), x2)
U52Active(x1, x2) → U52(x1, x2)
mark(U53(x1)) → U53Active(mark(x1))
U53Active(x1) → U53(x1)
mark(U61(x1, x2)) → U61Active(mark(x1), x2)
U61Active(x1, x2) → U61(x1, x2)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatIListKind(x1)) → isNatIListKindActive(x1)
isNatIListKindActive(x1) → isNatIListKind(x1)
mark(isNatKind(x1)) → isNatKindActive(x1)
isNatKindActive(x1) → isNatKind(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, V1) → U12Active(isNatListActive(V1))
U12Active(tt) → tt
U21Active(tt, V1) → U22Active(isNatActive(V1))
U22Active(tt) → tt
U31Active(tt, V) → U32Active(isNatListActive(V))
U32Active(tt) → tt
U41Active(tt, V1, V2) → U42Active(isNatActive(V1), V2)
U42Active(tt, V2) → U43Active(isNatIListActive(V2))
U43Active(tt) → tt
U51Active(tt, V1, V2) → U52Active(isNatActive(V1), V2)
U52Active(tt, V2) → U53Active(isNatListActive(V2))
U53Active(tt) → tt
U61Active(tt, L) → s(lengthActive(mark(L)))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → U11Active(isNatIListKindActive(V1), V1)
isNatActive(s(V1)) → U21Active(isNatKindActive(V1), V1)
isNatIListActive(V) → U31Active(isNatIListKindActive(V), V)
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → U41Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
isNatIListKindActive(nil) → tt
isNatIListKindActive(zeros) → tt
isNatIListKindActive(cons(V1, V2)) → andActive(isNatKindActive(V1), isNatIListKind(V2))
isNatKindActive(0) → tt
isNatKindActive(length(V1)) → isNatIListKindActive(V1)
isNatKindActive(s(V1)) → isNatKindActive(V1)
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → U51Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U61Active(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

U61ACTIVE(tt, U52(x0, x1)) → LENGTHACTIVE(U52Active(mark(x0), x1))
U61ACTIVE(tt, U51(x0, x1, x2)) → LENGTHACTIVE(U51Active(mark(x0), x1, x2))
U61ACTIVE(tt, U32(x0)) → LENGTHACTIVE(U32Active(mark(x0)))
U61ACTIVE(tt, U21(x0, x1)) → LENGTHACTIVE(U21Active(mark(x0), x1))
U61ACTIVE(tt, U42(x0, x1)) → LENGTHACTIVE(U42Active(mark(x0), x1))
U61ACTIVE(tt, U11(x0, x1)) → LENGTHACTIVE(U11Active(mark(x0), x1))
U61ACTIVE(tt, U22(x0)) → LENGTHACTIVE(U22Active(mark(x0)))
U61ACTIVE(tt, U12(x0)) → LENGTHACTIVE(U12Active(mark(x0)))
U61ACTIVE(tt, U31(x0, x1)) → LENGTHACTIVE(U31Active(mark(x0), x1))
U61ACTIVE(tt, isNatIList(x0)) → LENGTHACTIVE(isNatIListActive(x0))
U61ACTIVE(tt, U43(x0)) → LENGTHACTIVE(U43Active(mark(x0)))
U61ACTIVE(tt, U53(x0)) → LENGTHACTIVE(U53Active(mark(x0)))
U61ACTIVE(tt, U41(x0, x1, x2)) → LENGTHACTIVE(U41Active(mark(x0), x1, x2))
U61ACTIVE(tt, isNat(x0)) → LENGTHACTIVE(isNatActive(x0))
U61ACTIVE(tt, isNatList(x0)) → LENGTHACTIVE(isNatListActive(x0))

The remaining pairs can at least be oriented weakly.

U61ACTIVE(tt, isNatIListKind(x0)) → LENGTHACTIVE(isNatIListKindActive(x0))
U61ACTIVE(tt, isNatKind(x0)) → LENGTHACTIVE(isNatKindActive(x0))
U61ACTIVE(tt, zeros) → LENGTHACTIVE(cons(0, zeros))
LENGTHACTIVE(cons(N, L)) → U61ACTIVE(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)
U61ACTIVE(tt, and(x0, x1)) → LENGTHACTIVE(andActive(mark(x0), x1))
U61ACTIVE(tt, cons(x0, x1)) → LENGTHACTIVE(cons(mark(x0), x1))

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(LENGTHACTIVE(x₁)) = x₁
POL(U11(x₁, x₂)) = 0
POL(U11Active(x₁, x₂)) = 0
POL(U12(x₁)) = 0
POL(U12Active(x₁)) = 0
POL(U21(x₁, x₂)) = 0
POL(U21Active(x₁, x₂)) = 0
POL(U22(x₁)) = 0
POL(U22Active(x₁)) = 0
POL(U31(x₁, x₂)) = 0
POL(U31Active(x₁, x₂)) = 0
POL(U32(x₁)) = 0
POL(U32Active(x₁)) = 0
POL(U41(x₁, x₂, x₃)) = 0
POL(U41Active(x₁, x₂, x₃)) = 0
POL(U42(x₁, x₂)) = 0
POL(U42Active(x₁, x₂)) = 0
POL(U43(x₁)) = 0
POL(U43Active(x₁)) = 0
POL(U51(x₁, x₂, x₃)) = 0
POL(U51Active(x₁, x₂, x₃)) = 0
POL(U52(x₁, x₂)) = 0
POL(U52Active(x₁, x₂)) = 0
POL(U53(x₁)) = 0
POL(U53Active(x₁)) = 0
POL(U61(x₁, x₂)) = 0
POL(U61ACTIVE(x₁, x₂)) = 1
POL(U61Active(x₁, x₂)) = 0
POL(and(x₁, x₂)) = 0
POL(andActive(x₁, x₂)) = 1
POL(cons(x₁, x₂)) = 1
POL(isNat(x₁)) = 0
POL(isNatActive(x₁)) = 0
POL(isNatIList(x₁)) = 0
POL(isNatIListActive(x₁)) = 0
POL(isNatIListKind(x₁)) = 0
POL(isNatIListKindActive(x₁)) = 1
POL(isNatKind(x₁)) = 0
POL(isNatKindActive(x₁)) = 1
POL(isNatList(x₁)) = 0
POL(isNatListActive(x₁)) = 0
POL(length(x₁)) = x₁
POL(lengthActive(x₁)) = x₁
POL(mark(x₁)) = 1
POL(nil) = 1
POL(s(x₁)) = 0
POL(tt) = 0
POL(zeros) = 0
POL(zerosActive) = 1

The following usable rules [17] were oriented:

isNatKindActive(0) → tt
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → U41Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
mark(zeros) → zerosActive
isNatIListKindActive(nil) → tt
zerosActive → zeros
isNatIListKindActive(zeros) → tt
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → U51Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U61Active(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
isNatKindActive(length(V1)) → isNatIListKindActive(V1)
isNatIListKindActive(cons(V1, V2)) → andActive(isNatKindActive(V1), isNatIListKind(V2))
mark(isNatKind(x1)) → isNatKindActive(x1)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(tt, X) → mark(X)
mark(isNatIListKind(x1)) → isNatIListKindActive(x1)
isNatKindActive(s(V1)) → isNatKindActive(V1)
andActive(x1, x2) → and(x1, x2)
mark(U61(x1, x2)) → U61Active(mark(x1), x2)
U61Active(x1, x2) → U61(x1, x2)
mark(U53(x1)) → U53Active(mark(x1))
U53Active(x1) → U53(x1)
mark(U52(x1, x2)) → U52Active(mark(x1), x2)
U52Active(x1, x2) → U52(x1, x2)
mark(U51(x1, x2, x3)) → U51Active(mark(x1), x2, x3)
U51Active(x1, x2, x3) → U51(x1, x2, x3)
mark(U43(x1)) → U43Active(mark(x1))
U43Active(x1) → U43(x1)
U42Active(x1, x2) → U42(x1, x2)
mark(U42(x1, x2)) → U42Active(mark(x1), x2)
U41Active(x1, x2, x3) → U41(x1, x2, x3)
mark(U41(x1, x2, x3)) → U41Active(mark(x1), x2, x3)
U32Active(x1) → U32(x1)
mark(U32(x1)) → U32Active(mark(x1))
U31Active(x1, x2) → U31(x1, x2)
mark(U31(x1, x2)) → U31Active(mark(x1), x2)
U22Active(x1) → U22(x1)
mark(U22(x1)) → U22Active(mark(x1))
U21Active(x1, x2) → U21(x1, x2)
mark(U21(x1, x2)) → U21Active(mark(x1), x2)
U12Active(x1) → U12(x1)
mark(U12(x1)) → U12Active(mark(x1))
U11Active(x1, x2) → U11(x1, x2)
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
isNatActive(0) → tt
isNatActive(length(V1)) → U11Active(isNatIListKindActive(V1), V1)
isNatActive(s(V1)) → U21Active(isNatKindActive(V1), V1)
isNatIListActive(V) → U31Active(isNatIListKindActive(V), V)
U52Active(tt, V2) → U53Active(isNatListActive(V2))
U53Active(tt) → tt
U61Active(tt, L) → s(lengthActive(mark(L)))
U41Active(tt, V1, V2) → U42Active(isNatActive(V1), V2)
U42Active(tt, V2) → U43Active(isNatIListActive(V2))
U43Active(tt) → tt
U51Active(tt, V1, V2) → U52Active(isNatActive(V1), V2)
U21Active(tt, V1) → U22Active(isNatActive(V1))
U22Active(tt) → tt
U31Active(tt, V) → U32Active(isNatListActive(V))
U32Active(tt) → tt
zerosActive → cons(0, zeros)
mark(nil) → nil
U12Active(tt) → tt
U11Active(tt, V1) → U12Active(isNatListActive(V1))
mark(0) → 0
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(s(x1)) → s(mark(x1))
mark(tt) → tt
isNatListActive(x1) → isNatList(x1)
mark(isNatList(x1)) → isNatListActive(x1)
lengthActive(x1) → length(x1)
mark(length(x1)) → lengthActive(mark(x1))
isNatIListKindActive(x1) → isNatIListKind(x1)
isNatKindActive(x1) → isNatKind(x1)

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

U61ACTIVE(tt, and(x0, x1)) → LENGTHACTIVE(andActive(mark(x0), x1))
U61ACTIVE(tt, isNatIListKind(x0)) → LENGTHACTIVE(isNatIListKindActive(x0))
U61ACTIVE(tt, cons(x0, x1)) → LENGTHACTIVE(cons(mark(x0), x1))
U61ACTIVE(tt, isNatKind(x0)) → LENGTHACTIVE(isNatKindActive(x0))
U61ACTIVE(tt, zeros) → LENGTHACTIVE(cons(0, zeros))
LENGTHACTIVE(cons(N, L)) → U61ACTIVE(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U12(x1)) → U12Active(mark(x1))
U12Active(x1) → U12(x1)
mark(U21(x1, x2)) → U21Active(mark(x1), x2)
U21Active(x1, x2) → U21(x1, x2)
mark(U22(x1)) → U22Active(mark(x1))
U22Active(x1) → U22(x1)
mark(U31(x1, x2)) → U31Active(mark(x1), x2)
U31Active(x1, x2) → U31(x1, x2)
mark(U32(x1)) → U32Active(mark(x1))
U32Active(x1) → U32(x1)
mark(U41(x1, x2, x3)) → U41Active(mark(x1), x2, x3)
U41Active(x1, x2, x3) → U41(x1, x2, x3)
mark(U42(x1, x2)) → U42Active(mark(x1), x2)
U42Active(x1, x2) → U42(x1, x2)
mark(U43(x1)) → U43Active(mark(x1))
U43Active(x1) → U43(x1)
mark(U51(x1, x2, x3)) → U51Active(mark(x1), x2, x3)
U51Active(x1, x2, x3) → U51(x1, x2, x3)
mark(U52(x1, x2)) → U52Active(mark(x1), x2)
U52Active(x1, x2) → U52(x1, x2)
mark(U53(x1)) → U53Active(mark(x1))
U53Active(x1) → U53(x1)
mark(U61(x1, x2)) → U61Active(mark(x1), x2)
U61Active(x1, x2) → U61(x1, x2)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatIListKind(x1)) → isNatIListKindActive(x1)
isNatIListKindActive(x1) → isNatIListKind(x1)
mark(isNatKind(x1)) → isNatKindActive(x1)
isNatKindActive(x1) → isNatKind(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, V1) → U12Active(isNatListActive(V1))
U12Active(tt) → tt
U21Active(tt, V1) → U22Active(isNatActive(V1))
U22Active(tt) → tt
U31Active(tt, V) → U32Active(isNatListActive(V))
U32Active(tt) → tt
U41Active(tt, V1, V2) → U42Active(isNatActive(V1), V2)
U42Active(tt, V2) → U43Active(isNatIListActive(V2))
U43Active(tt) → tt
U51Active(tt, V1, V2) → U52Active(isNatActive(V1), V2)
U52Active(tt, V2) → U53Active(isNatListActive(V2))
U53Active(tt) → tt
U61Active(tt, L) → s(lengthActive(mark(L)))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → U11Active(isNatIListKindActive(V1), V1)
isNatActive(s(V1)) → U21Active(isNatKindActive(V1), V1)
isNatIListActive(V) → U31Active(isNatIListKindActive(V), V)
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → U41Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
isNatIListKindActive(nil) → tt
isNatIListKindActive(zeros) → tt
isNatIListKindActive(cons(V1, V2)) → andActive(isNatKindActive(V1), isNatIListKind(V2))
isNatKindActive(0) → tt
isNatKindActive(length(V1)) → isNatIListKindActive(V1)
isNatKindActive(s(V1)) → isNatKindActive(V1)
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → U51Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U61Active(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

U61ACTIVE(tt, and(x0, x1)) → LENGTHACTIVE(andActive(mark(x0), x1))
U61ACTIVE(tt, cons(x0, x1)) → LENGTHACTIVE(cons(mark(x0), x1))

The remaining pairs can at least be oriented weakly.

U61ACTIVE(tt, isNatIListKind(x0)) → LENGTHACTIVE(isNatIListKindActive(x0))
U61ACTIVE(tt, isNatKind(x0)) → LENGTHACTIVE(isNatKindActive(x0))
U61ACTIVE(tt, zeros) → LENGTHACTIVE(cons(0, zeros))
LENGTHACTIVE(cons(N, L)) → U61ACTIVE(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(LENGTHACTIVE(x₁)) = x₁
POL(U11(x₁, x₂)) = 0
POL(U11Active(x₁, x₂)) = 0
POL(U12(x₁)) = 0
POL(U12Active(x₁)) = 0
POL(U21(x₁, x₂)) = 0
POL(U21Active(x₁, x₂)) = 0
POL(U22(x₁)) = 0
POL(U22Active(x₁)) = 0
POL(U31(x₁, x₂)) = 0
POL(U31Active(x₁, x₂)) = 0
POL(U32(x₁)) = 0
POL(U32Active(x₁)) = 0
POL(U41(x₁, x₂, x₃)) = 1
POL(U41Active(x₁, x₂, x₃)) = 1
POL(U42(x₁, x₂)) = 0
POL(U42Active(x₁, x₂)) = 0
POL(U43(x₁)) = 0
POL(U43Active(x₁)) = 0
POL(U51(x₁, x₂, x₃)) = 0
POL(U51Active(x₁, x₂, x₃)) = 0
POL(U52(x₁, x₂)) = 0
POL(U52Active(x₁, x₂)) = 0
POL(U53(x₁)) = 0
POL(U53Active(x₁)) = 0
POL(U61(x₁, x₂)) = 0
POL(U61ACTIVE(x₁, x₂)) = 1 + x₂
POL(U61Active(x₁, x₂)) = 0
POL(and(x₁, x₂)) = 1 + x₂
POL(andActive(x₁, x₂)) = 1 + x₂
POL(cons(x₁, x₂)) = 1 + x₂
POL(isNat(x₁)) = 0
POL(isNatActive(x₁)) = 0
POL(isNatIList(x₁)) = 1
POL(isNatIListActive(x₁)) = 1
POL(isNatIListKind(x₁)) = 0
POL(isNatIListKindActive(x₁)) = 1
POL(isNatKind(x₁)) = 0
POL(isNatKindActive(x₁)) = 1
POL(isNatList(x₁)) = 0
POL(isNatListActive(x₁)) = 0
POL(length(x₁)) = 0
POL(lengthActive(x₁)) = 0
POL(mark(x₁)) = 1 + x₁
POL(nil) = 1
POL(s(x₁)) = 0
POL(tt) = 0
POL(zeros) = 0
POL(zerosActive) = 1

The following usable rules [17] were oriented:

isNatKindActive(0) → tt
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → U41Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
isNatIListKindActive(nil) → tt
mark(zeros) → zerosActive
zerosActive → zeros
isNatIListKindActive(zeros) → tt
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → U51Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U61Active(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
isNatKindActive(length(V1)) → isNatIListKindActive(V1)
isNatIListKindActive(cons(V1, V2)) → andActive(isNatKindActive(V1), isNatIListKind(V2))
mark(isNatKind(x1)) → isNatKindActive(x1)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(tt, X) → mark(X)
mark(isNatIListKind(x1)) → isNatIListKindActive(x1)
isNatKindActive(s(V1)) → isNatKindActive(V1)
andActive(x1, x2) → and(x1, x2)
mark(U61(x1, x2)) → U61Active(mark(x1), x2)
U61Active(x1, x2) → U61(x1, x2)
mark(U53(x1)) → U53Active(mark(x1))
U53Active(x1) → U53(x1)
mark(U52(x1, x2)) → U52Active(mark(x1), x2)
U52Active(x1, x2) → U52(x1, x2)
mark(U51(x1, x2, x3)) → U51Active(mark(x1), x2, x3)
U51Active(x1, x2, x3) → U51(x1, x2, x3)
mark(U43(x1)) → U43Active(mark(x1))
U43Active(x1) → U43(x1)
U42Active(x1, x2) → U42(x1, x2)
mark(U42(x1, x2)) → U42Active(mark(x1), x2)
U41Active(x1, x2, x3) → U41(x1, x2, x3)
mark(U41(x1, x2, x3)) → U41Active(mark(x1), x2, x3)
U32Active(x1) → U32(x1)
mark(U32(x1)) → U32Active(mark(x1))
U31Active(x1, x2) → U31(x1, x2)
mark(U31(x1, x2)) → U31Active(mark(x1), x2)
U22Active(x1) → U22(x1)
mark(U22(x1)) → U22Active(mark(x1))
U21Active(x1, x2) → U21(x1, x2)
mark(U21(x1, x2)) → U21Active(mark(x1), x2)
U12Active(x1) → U12(x1)
mark(U12(x1)) → U12Active(mark(x1))
U11Active(x1, x2) → U11(x1, x2)
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
isNatActive(0) → tt
isNatActive(length(V1)) → U11Active(isNatIListKindActive(V1), V1)
isNatActive(s(V1)) → U21Active(isNatKindActive(V1), V1)
isNatIListActive(V) → U31Active(isNatIListKindActive(V), V)
U52Active(tt, V2) → U53Active(isNatListActive(V2))
U53Active(tt) → tt
U61Active(tt, L) → s(lengthActive(mark(L)))
U41Active(tt, V1, V2) → U42Active(isNatActive(V1), V2)
U42Active(tt, V2) → U43Active(isNatIListActive(V2))
U43Active(tt) → tt
U51Active(tt, V1, V2) → U52Active(isNatActive(V1), V2)
U21Active(tt, V1) → U22Active(isNatActive(V1))
U22Active(tt) → tt
U31Active(tt, V) → U32Active(isNatListActive(V))
U32Active(tt) → tt
zerosActive → cons(0, zeros)
mark(nil) → nil
U12Active(tt) → tt
U11Active(tt, V1) → U12Active(isNatListActive(V1))
mark(0) → 0
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(s(x1)) → s(mark(x1))
mark(tt) → tt
isNatListActive(x1) → isNatList(x1)
mark(isNatList(x1)) → isNatListActive(x1)
lengthActive(x1) → length(x1)
mark(length(x1)) → lengthActive(mark(x1))
isNatIListKindActive(x1) → isNatIListKind(x1)
isNatKindActive(x1) → isNatKind(x1)

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ QDPOrderProof

                                                  ↳ QDP

                                                    ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

U61ACTIVE(tt, isNatIListKind(x0)) → LENGTHACTIVE(isNatIListKindActive(x0))
U61ACTIVE(tt, isNatKind(x0)) → LENGTHACTIVE(isNatKindActive(x0))
U61ACTIVE(tt, zeros) → LENGTHACTIVE(cons(0, zeros))
LENGTHACTIVE(cons(N, L)) → U61ACTIVE(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U12(x1)) → U12Active(mark(x1))
U12Active(x1) → U12(x1)
mark(U21(x1, x2)) → U21Active(mark(x1), x2)
U21Active(x1, x2) → U21(x1, x2)
mark(U22(x1)) → U22Active(mark(x1))
U22Active(x1) → U22(x1)
mark(U31(x1, x2)) → U31Active(mark(x1), x2)
U31Active(x1, x2) → U31(x1, x2)
mark(U32(x1)) → U32Active(mark(x1))
U32Active(x1) → U32(x1)
mark(U41(x1, x2, x3)) → U41Active(mark(x1), x2, x3)
U41Active(x1, x2, x3) → U41(x1, x2, x3)
mark(U42(x1, x2)) → U42Active(mark(x1), x2)
U42Active(x1, x2) → U42(x1, x2)
mark(U43(x1)) → U43Active(mark(x1))
U43Active(x1) → U43(x1)
mark(U51(x1, x2, x3)) → U51Active(mark(x1), x2, x3)
U51Active(x1, x2, x3) → U51(x1, x2, x3)
mark(U52(x1, x2)) → U52Active(mark(x1), x2)
U52Active(x1, x2) → U52(x1, x2)
mark(U53(x1)) → U53Active(mark(x1))
U53Active(x1) → U53(x1)
mark(U61(x1, x2)) → U61Active(mark(x1), x2)
U61Active(x1, x2) → U61(x1, x2)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatIListKind(x1)) → isNatIListKindActive(x1)
isNatIListKindActive(x1) → isNatIListKind(x1)
mark(isNatKind(x1)) → isNatKindActive(x1)
isNatKindActive(x1) → isNatKind(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, V1) → U12Active(isNatListActive(V1))
U12Active(tt) → tt
U21Active(tt, V1) → U22Active(isNatActive(V1))
U22Active(tt) → tt
U31Active(tt, V) → U32Active(isNatListActive(V))
U32Active(tt) → tt
U41Active(tt, V1, V2) → U42Active(isNatActive(V1), V2)
U42Active(tt, V2) → U43Active(isNatIListActive(V2))
U43Active(tt) → tt
U51Active(tt, V1, V2) → U52Active(isNatActive(V1), V2)
U52Active(tt, V2) → U53Active(isNatListActive(V2))
U53Active(tt) → tt
U61Active(tt, L) → s(lengthActive(mark(L)))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → U11Active(isNatIListKindActive(V1), V1)
isNatActive(s(V1)) → U21Active(isNatKindActive(V1), V1)
isNatIListActive(V) → U31Active(isNatIListKindActive(V), V)
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → U41Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
isNatIListKindActive(nil) → tt
isNatIListKindActive(zeros) → tt
isNatIListKindActive(cons(V1, V2)) → andActive(isNatKindActive(V1), isNatIListKind(V2))
isNatKindActive(0) → tt
isNatKindActive(length(V1)) → isNatIListKindActive(V1)
isNatKindActive(s(V1)) → isNatKindActive(V1)
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → U51Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U61Active(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

U61ACTIVE(tt, zeros) → LENGTHACTIVE(cons(0, zeros))

The remaining pairs can at least be oriented weakly.

U61ACTIVE(tt, isNatIListKind(x0)) → LENGTHACTIVE(isNatIListKindActive(x0))
U61ACTIVE(tt, isNatKind(x0)) → LENGTHACTIVE(isNatKindActive(x0))
LENGTHACTIVE(cons(N, L)) → U61ACTIVE(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(LENGTHACTIVE(x₁)) = x₁
POL(U11(x₁, x₂)) = x₁
POL(U11Active(x₁, x₂)) = x₁
POL(U12(x₁)) = 0
POL(U12Active(x₁)) = 1
POL(U21(x₁, x₂)) = 0
POL(U21Active(x₁, x₂)) = 1
POL(U22(x₁)) = 1
POL(U22Active(x₁)) = 1
POL(U31(x₁, x₂)) = 1
POL(U31Active(x₁, x₂)) = 1
POL(U32(x₁)) = 0
POL(U32Active(x₁)) = 1
POL(U41(x₁, x₂, x₃)) = 1
POL(U41Active(x₁, x₂, x₃)) = 1
POL(U42(x₁, x₂)) = x₁
POL(U42Active(x₁, x₂)) = x₁
POL(U43(x₁)) = 1
POL(U43Active(x₁)) = 1
POL(U51(x₁, x₂, x₃)) = x₃
POL(U51Active(x₁, x₂, x₃)) = x₃
POL(U52(x₁, x₂)) = x₂
POL(U52Active(x₁, x₂)) = x₂
POL(U53(x₁)) = x₁
POL(U53Active(x₁)) = x₁
POL(U61(x₁, x₂)) = 0
POL(U61ACTIVE(x₁, x₂)) = x₁
POL(U61Active(x₁, x₂)) = 0
POL(and(x₁, x₂)) = x₁ + x₂
POL(andActive(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = x₂
POL(isNat(x₁)) = 0
POL(isNatActive(x₁)) = 1
POL(isNatIList(x₁)) = 1
POL(isNatIListActive(x₁)) = 1
POL(isNatIListKind(x₁)) = 0
POL(isNatIListKindActive(x₁)) = 1
POL(isNatKind(x₁)) = 0
POL(isNatKindActive(x₁)) = 1
POL(isNatList(x₁)) = x₁
POL(isNatListActive(x₁)) = x₁
POL(length(x₁)) = 0
POL(lengthActive(x₁)) = 0
POL(mark(x₁)) = 1 + x₁
POL(nil) = 1
POL(s(x₁)) = 0
POL(tt) = 1
POL(zeros) = 0
POL(zerosActive) = 1

The following usable rules [17] were oriented:

isNatKindActive(0) → tt
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → U41Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
isNatIListKindActive(nil) → tt
mark(zeros) → zerosActive
zerosActive → zeros
isNatIListKindActive(zeros) → tt
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → U51Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U61Active(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
isNatKindActive(length(V1)) → isNatIListKindActive(V1)
isNatIListKindActive(cons(V1, V2)) → andActive(isNatKindActive(V1), isNatIListKind(V2))
mark(isNatKind(x1)) → isNatKindActive(x1)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(tt, X) → mark(X)
mark(isNatIListKind(x1)) → isNatIListKindActive(x1)
isNatKindActive(s(V1)) → isNatKindActive(V1)
andActive(x1, x2) → and(x1, x2)
mark(U61(x1, x2)) → U61Active(mark(x1), x2)
U61Active(x1, x2) → U61(x1, x2)
mark(U53(x1)) → U53Active(mark(x1))
U53Active(x1) → U53(x1)
mark(U52(x1, x2)) → U52Active(mark(x1), x2)
U52Active(x1, x2) → U52(x1, x2)
mark(U51(x1, x2, x3)) → U51Active(mark(x1), x2, x3)
U51Active(x1, x2, x3) → U51(x1, x2, x3)
mark(U43(x1)) → U43Active(mark(x1))
U43Active(x1) → U43(x1)
U42Active(x1, x2) → U42(x1, x2)
mark(U42(x1, x2)) → U42Active(mark(x1), x2)
U41Active(x1, x2, x3) → U41(x1, x2, x3)
mark(U41(x1, x2, x3)) → U41Active(mark(x1), x2, x3)
U32Active(x1) → U32(x1)
mark(U32(x1)) → U32Active(mark(x1))
U31Active(x1, x2) → U31(x1, x2)
mark(U31(x1, x2)) → U31Active(mark(x1), x2)
U22Active(x1) → U22(x1)
mark(U22(x1)) → U22Active(mark(x1))
U21Active(x1, x2) → U21(x1, x2)
mark(U21(x1, x2)) → U21Active(mark(x1), x2)
U12Active(x1) → U12(x1)
mark(U12(x1)) → U12Active(mark(x1))
U11Active(x1, x2) → U11(x1, x2)
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
isNatActive(0) → tt
isNatActive(length(V1)) → U11Active(isNatIListKindActive(V1), V1)
isNatActive(s(V1)) → U21Active(isNatKindActive(V1), V1)
isNatIListActive(V) → U31Active(isNatIListKindActive(V), V)
U52Active(tt, V2) → U53Active(isNatListActive(V2))
U53Active(tt) → tt
U61Active(tt, L) → s(lengthActive(mark(L)))
U41Active(tt, V1, V2) → U42Active(isNatActive(V1), V2)
U42Active(tt, V2) → U43Active(isNatIListActive(V2))
U43Active(tt) → tt
U51Active(tt, V1, V2) → U52Active(isNatActive(V1), V2)
U21Active(tt, V1) → U22Active(isNatActive(V1))
U22Active(tt) → tt
U31Active(tt, V) → U32Active(isNatListActive(V))
U32Active(tt) → tt
zerosActive → cons(0, zeros)
mark(nil) → nil
U12Active(tt) → tt
U11Active(tt, V1) → U12Active(isNatListActive(V1))
mark(0) → 0
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(s(x1)) → s(mark(x1))
mark(tt) → tt
isNatListActive(x1) → isNatList(x1)
mark(isNatList(x1)) → isNatListActive(x1)
lengthActive(x1) → length(x1)
mark(length(x1)) → lengthActive(mark(x1))
isNatIListKindActive(x1) → isNatIListKind(x1)
isNatKindActive(x1) → isNatKind(x1)

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ QDPOrderProof

                                                  ↳ QDP

                                                    ↳ QDPOrderProof

                                                      ↳ QDP

                                                        ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

U61ACTIVE(tt, isNatIListKind(x0)) → LENGTHACTIVE(isNatIListKindActive(x0))
U61ACTIVE(tt, isNatKind(x0)) → LENGTHACTIVE(isNatKindActive(x0))
LENGTHACTIVE(cons(N, L)) → U61ACTIVE(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U12(x1)) → U12Active(mark(x1))
U12Active(x1) → U12(x1)
mark(U21(x1, x2)) → U21Active(mark(x1), x2)
U21Active(x1, x2) → U21(x1, x2)
mark(U22(x1)) → U22Active(mark(x1))
U22Active(x1) → U22(x1)
mark(U31(x1, x2)) → U31Active(mark(x1), x2)
U31Active(x1, x2) → U31(x1, x2)
mark(U32(x1)) → U32Active(mark(x1))
U32Active(x1) → U32(x1)
mark(U41(x1, x2, x3)) → U41Active(mark(x1), x2, x3)
U41Active(x1, x2, x3) → U41(x1, x2, x3)
mark(U42(x1, x2)) → U42Active(mark(x1), x2)
U42Active(x1, x2) → U42(x1, x2)
mark(U43(x1)) → U43Active(mark(x1))
U43Active(x1) → U43(x1)
mark(U51(x1, x2, x3)) → U51Active(mark(x1), x2, x3)
U51Active(x1, x2, x3) → U51(x1, x2, x3)
mark(U52(x1, x2)) → U52Active(mark(x1), x2)
U52Active(x1, x2) → U52(x1, x2)
mark(U53(x1)) → U53Active(mark(x1))
U53Active(x1) → U53(x1)
mark(U61(x1, x2)) → U61Active(mark(x1), x2)
U61Active(x1, x2) → U61(x1, x2)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatIListKind(x1)) → isNatIListKindActive(x1)
isNatIListKindActive(x1) → isNatIListKind(x1)
mark(isNatKind(x1)) → isNatKindActive(x1)
isNatKindActive(x1) → isNatKind(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, V1) → U12Active(isNatListActive(V1))
U12Active(tt) → tt
U21Active(tt, V1) → U22Active(isNatActive(V1))
U22Active(tt) → tt
U31Active(tt, V) → U32Active(isNatListActive(V))
U32Active(tt) → tt
U41Active(tt, V1, V2) → U42Active(isNatActive(V1), V2)
U42Active(tt, V2) → U43Active(isNatIListActive(V2))
U43Active(tt) → tt
U51Active(tt, V1, V2) → U52Active(isNatActive(V1), V2)
U52Active(tt, V2) → U53Active(isNatListActive(V2))
U53Active(tt) → tt
U61Active(tt, L) → s(lengthActive(mark(L)))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → U11Active(isNatIListKindActive(V1), V1)
isNatActive(s(V1)) → U21Active(isNatKindActive(V1), V1)
isNatIListActive(V) → U31Active(isNatIListKindActive(V), V)
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → U41Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
isNatIListKindActive(nil) → tt
isNatIListKindActive(zeros) → tt
isNatIListKindActive(cons(V1, V2)) → andActive(isNatKindActive(V1), isNatIListKind(V2))
isNatKindActive(0) → tt
isNatKindActive(length(V1)) → isNatIListKindActive(V1)
isNatKindActive(s(V1)) → isNatKindActive(V1)
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → U51Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U61Active(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

U61ACTIVE(tt, isNatIListKind(x0)) → LENGTHACTIVE(isNatIListKindActive(x0))
U61ACTIVE(tt, isNatKind(x0)) → LENGTHACTIVE(isNatKindActive(x0))

The remaining pairs can at least be oriented weakly.

LENGTHACTIVE(cons(N, L)) → U61ACTIVE(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(LENGTHACTIVE(x₁)) = x₁
POL(U11(x₁, x₂)) = 0
POL(U11Active(x₁, x₂)) = 0
POL(U12(x₁)) = 0
POL(U12Active(x₁)) = 0
POL(U21(x₁, x₂)) = 0
POL(U21Active(x₁, x₂)) = 0
POL(U22(x₁)) = 0
POL(U22Active(x₁)) = 0
POL(U31(x₁, x₂)) = 0
POL(U31Active(x₁, x₂)) = 0
POL(U32(x₁)) = 0
POL(U32Active(x₁)) = 0
POL(U41(x₁, x₂, x₃)) = 0
POL(U41Active(x₁, x₂, x₃)) = 0
POL(U42(x₁, x₂)) = 0
POL(U42Active(x₁, x₂)) = 0
POL(U43(x₁)) = 0
POL(U43Active(x₁)) = 0
POL(U51(x₁, x₂, x₃)) = x₁
POL(U51Active(x₁, x₂, x₃)) = x₁
POL(U52(x₁, x₂)) = 0
POL(U52Active(x₁, x₂)) = 0
POL(U53(x₁)) = x₁
POL(U53Active(x₁)) = x₁
POL(U61(x₁, x₂)) = 1
POL(U61ACTIVE(x₁, x₂)) = 1
POL(U61Active(x₁, x₂)) = 1
POL(and(x₁, x₂)) = x₂
POL(andActive(x₁, x₂)) = x₂
POL(cons(x₁, x₂)) = 1
POL(isNat(x₁)) = 0
POL(isNatActive(x₁)) = 0
POL(isNatIList(x₁)) = 1
POL(isNatIListActive(x₁)) = 1
POL(isNatIListKind(x₁)) = 0
POL(isNatIListKindActive(x₁)) = 0
POL(isNatKind(x₁)) = 0
POL(isNatKindActive(x₁)) = 0
POL(isNatList(x₁)) = 0
POL(isNatListActive(x₁)) = 0
POL(length(x₁)) = 1
POL(lengthActive(x₁)) = 1
POL(mark(x₁)) = x₁
POL(nil) = 0
POL(s(x₁)) = 0
POL(tt) = 0
POL(zeros) = 1
POL(zerosActive) = 1

The following usable rules [17] were oriented:

isNatKindActive(0) → tt
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → U41Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
isNatIListKindActive(nil) → tt
mark(zeros) → zerosActive
zerosActive → zeros
isNatIListKindActive(zeros) → tt
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → U51Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U61Active(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
isNatKindActive(length(V1)) → isNatIListKindActive(V1)
isNatIListKindActive(cons(V1, V2)) → andActive(isNatKindActive(V1), isNatIListKind(V2))
mark(isNatKind(x1)) → isNatKindActive(x1)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(tt, X) → mark(X)
mark(isNatIListKind(x1)) → isNatIListKindActive(x1)
isNatKindActive(s(V1)) → isNatKindActive(V1)
andActive(x1, x2) → and(x1, x2)
mark(U61(x1, x2)) → U61Active(mark(x1), x2)
U61Active(x1, x2) → U61(x1, x2)
mark(U53(x1)) → U53Active(mark(x1))
U53Active(x1) → U53(x1)
mark(U52(x1, x2)) → U52Active(mark(x1), x2)
U52Active(x1, x2) → U52(x1, x2)
mark(U51(x1, x2, x3)) → U51Active(mark(x1), x2, x3)
U51Active(x1, x2, x3) → U51(x1, x2, x3)
mark(U43(x1)) → U43Active(mark(x1))
U43Active(x1) → U43(x1)
U42Active(x1, x2) → U42(x1, x2)
mark(U42(x1, x2)) → U42Active(mark(x1), x2)
U41Active(x1, x2, x3) → U41(x1, x2, x3)
mark(U41(x1, x2, x3)) → U41Active(mark(x1), x2, x3)
U32Active(x1) → U32(x1)
mark(U32(x1)) → U32Active(mark(x1))
U31Active(x1, x2) → U31(x1, x2)
mark(U31(x1, x2)) → U31Active(mark(x1), x2)
U22Active(x1) → U22(x1)
mark(U22(x1)) → U22Active(mark(x1))
U21Active(x1, x2) → U21(x1, x2)
mark(U21(x1, x2)) → U21Active(mark(x1), x2)
U12Active(x1) → U12(x1)
mark(U12(x1)) → U12Active(mark(x1))
U11Active(x1, x2) → U11(x1, x2)
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
isNatActive(0) → tt
isNatActive(length(V1)) → U11Active(isNatIListKindActive(V1), V1)
isNatActive(s(V1)) → U21Active(isNatKindActive(V1), V1)
isNatIListActive(V) → U31Active(isNatIListKindActive(V), V)
U52Active(tt, V2) → U53Active(isNatListActive(V2))
U53Active(tt) → tt
U61Active(tt, L) → s(lengthActive(mark(L)))
U41Active(tt, V1, V2) → U42Active(isNatActive(V1), V2)
U42Active(tt, V2) → U43Active(isNatIListActive(V2))
U43Active(tt) → tt
U51Active(tt, V1, V2) → U52Active(isNatActive(V1), V2)
U21Active(tt, V1) → U22Active(isNatActive(V1))
U22Active(tt) → tt
U31Active(tt, V) → U32Active(isNatListActive(V))
U32Active(tt) → tt
zerosActive → cons(0, zeros)
mark(nil) → nil
U12Active(tt) → tt
U11Active(tt, V1) → U12Active(isNatListActive(V1))
mark(0) → 0
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(s(x1)) → s(mark(x1))
mark(tt) → tt
isNatListActive(x1) → isNatList(x1)
mark(isNatList(x1)) → isNatListActive(x1)
lengthActive(x1) → length(x1)
mark(length(x1)) → lengthActive(mark(x1))
isNatIListKindActive(x1) → isNatIListKind(x1)
isNatKindActive(x1) → isNatKind(x1)

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ QDP

                                        ↳ QDPOrderProof

                                          ↳ QDP

                                            ↳ QDPOrderProof

                                              ↳ QDP

                                                ↳ QDPOrderProof

                                                  ↳ QDP

                                                    ↳ QDPOrderProof

                                                      ↳ QDP

                                                        ↳ QDPOrderProof

                                                          ↳ QDP

                                                            ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

LENGTHACTIVE(cons(N, L)) → U61ACTIVE(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U12(x1)) → U12Active(mark(x1))
U12Active(x1) → U12(x1)
mark(U21(x1, x2)) → U21Active(mark(x1), x2)
U21Active(x1, x2) → U21(x1, x2)
mark(U22(x1)) → U22Active(mark(x1))
U22Active(x1) → U22(x1)
mark(U31(x1, x2)) → U31Active(mark(x1), x2)
U31Active(x1, x2) → U31(x1, x2)
mark(U32(x1)) → U32Active(mark(x1))
U32Active(x1) → U32(x1)
mark(U41(x1, x2, x3)) → U41Active(mark(x1), x2, x3)
U41Active(x1, x2, x3) → U41(x1, x2, x3)
mark(U42(x1, x2)) → U42Active(mark(x1), x2)
U42Active(x1, x2) → U42(x1, x2)
mark(U43(x1)) → U43Active(mark(x1))
U43Active(x1) → U43(x1)
mark(U51(x1, x2, x3)) → U51Active(mark(x1), x2, x3)
U51Active(x1, x2, x3) → U51(x1, x2, x3)
mark(U52(x1, x2)) → U52Active(mark(x1), x2)
U52Active(x1, x2) → U52(x1, x2)
mark(U53(x1)) → U53Active(mark(x1))
U53Active(x1) → U53(x1)
mark(U61(x1, x2)) → U61Active(mark(x1), x2)
U61Active(x1, x2) → U61(x1, x2)
mark(and(x1, x2)) → andActive(mark(x1), x2)
andActive(x1, x2) → and(x1, x2)
mark(isNat(x1)) → isNatActive(x1)
isNatActive(x1) → isNat(x1)
mark(isNatIList(x1)) → isNatIListActive(x1)
isNatIListActive(x1) → isNatIList(x1)
mark(isNatIListKind(x1)) → isNatIListKindActive(x1)
isNatIListKindActive(x1) → isNatIListKind(x1)
mark(isNatKind(x1)) → isNatKindActive(x1)
isNatKindActive(x1) → isNatKind(x1)
mark(isNatList(x1)) → isNatListActive(x1)
isNatListActive(x1) → isNatList(x1)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, V1) → U12Active(isNatListActive(V1))
U12Active(tt) → tt
U21Active(tt, V1) → U22Active(isNatActive(V1))
U22Active(tt) → tt
U31Active(tt, V) → U32Active(isNatListActive(V))
U32Active(tt) → tt
U41Active(tt, V1, V2) → U42Active(isNatActive(V1), V2)
U42Active(tt, V2) → U43Active(isNatIListActive(V2))
U43Active(tt) → tt
U51Active(tt, V1, V2) → U52Active(isNatActive(V1), V2)
U52Active(tt, V2) → U53Active(isNatListActive(V2))
U53Active(tt) → tt
U61Active(tt, L) → s(lengthActive(mark(L)))
andActive(tt, X) → mark(X)
isNatActive(0) → tt
isNatActive(length(V1)) → U11Active(isNatIListKindActive(V1), V1)
isNatActive(s(V1)) → U21Active(isNatKindActive(V1), V1)
isNatIListActive(V) → U31Active(isNatIListKindActive(V), V)
isNatIListActive(zeros) → tt
isNatIListActive(cons(V1, V2)) → U41Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
isNatIListKindActive(nil) → tt
isNatIListKindActive(zeros) → tt
isNatIListKindActive(cons(V1, V2)) → andActive(isNatKindActive(V1), isNatIListKind(V2))
isNatKindActive(0) → tt
isNatKindActive(length(V1)) → isNatIListKindActive(V1)
isNatKindActive(s(V1)) → isNatKindActive(V1)
isNatListActive(nil) → tt
isNatListActive(cons(V1, V2)) → U51Active(andActive(isNatKindActive(V1), isNatIListKind(V2)), V1, V2)
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U61Active(andActive(andActive(isNatListActive(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 1 less node.